:: deftheorem Def5 defines -VectSp_over PRVECT_1:def 5 :
for F being Field
for n being Nat
for b₃ being strict ModuleStr over F holds
( b₃ = n -VectSp_over F iff ( addLoopStr(# the carrier of b₃, the addF of b₃, the ZeroF of b₃ #) = n -Group_over F & the lmult of b₃ = n -Mult_over F ) );