:: deftheorem Def5 defines VecSp FIELD_4:def 6 :
for R being Ring
for S being RingExtension of R
for b₃ being strict ModuleStr over R holds
( b₃ = VecSp (S,R) iff ( the carrier of b₃ = the carrier of S & the addF of b₃ = the addF of S & the ZeroF of b₃ = 0. S & the lmult of b₃ = the multF of S | [: the carrier of R, the carrier of S:] ) );