(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 \}")