:: deftheorem Def2 defines Subspace VECTSP_4:def 2 :
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V, b₃ being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds
( b₃ is Subspace of V iff ( the carrier of b₃ c= the carrier of V & 0. b₃ = 0. V & the addF of b₃ = the addF of V || the carrier of b₃ & the lmult of b₃ = the lmult of V | [: the carrier of GF, the carrier of b₃:] ) );