(def-language vector-space-language 
    (base-types vv)
    (embedded-languages fields)
    (constants
      (++ (vv vv vv))
      (v0 vv)
      (** (kk vv vv))))

(def-theory vector-spaces 
    (language vector-space-language)
    (component-theories fields h-o-real-arithmetic)
    (axioms
      (vector-plus-totality
        "total_q{++,[vv, vv, vv]}" d-r-convergence transportable-macete)
      (vector-plus-associativity
        "forall(x,y,z:vv, (x ++ y) ++ z = x ++ (y ++ z))" transportable-macete)
      (vector-plus-commutativity
        "forall(x,y:vv, x ++ y  =  y ++ x)" transportable-macete)
      (vector-zero-identity
        "forall(x:vv, x ++ v0=x)" transportable-macete)
      (vector-times-totality
        "total_q{**,[kk, vv, vv]}" d-r-convergence transportable-macete)
      (vector-times-associativity
        "forall(x,y:kk, z:vv, (x *_kk y)**z = x ** (y ** z))" transportable-macete)
      (vector-times-left-distributivity
        "forall(x,y:vv, a:kk, a ** (x ++ y) = (a**x) ++ (a**y))" transportable-macete)
      (vector-times-right-distributivity
        "forall(a,b:kk, x:vv, (a +_kk b)**x = (a**x) ++ (b**x))" transportable-macete)
      (scalar-multiplication-by-zero
        "forall(x:vv, o_kk ** x = v0)" transportable-macete)
      (scalar-multiplication-by-one
        "forall(x:vv, i_kk ** x = x)" transportable-macete)))
(make-tex-correspondence "vv" " \{ \\bf v \}")