:: deftheorem Def2 defines Lin VECTSP_7:def 2 :
for GF being Ring
for V being LeftMod of GF
for A being Subset of V
for b₄ being strict Subspace of V holds
( b₄ = Lin A iff the carrier of b₄ = { (Sum l) where l is Linear_Combination of A : verum } );