:: deftheorem DEF defines ^* VECTSP13:def 7 :
for R being Ring
for n being Nat
for b₃ being strict ModuleStr over R holds
( b₃ = R ^* n iff ( the carrier of b₃ = n -tuples_on the carrier of R & the addF of b₃ = vector_add (n,R) & the ZeroF of b₃ = n |-> (0. R) & the lmult of b₃ = vector_mult (n,R) ) );