theorem :: ZMODUL02:18

for R being Ring
for V being LeftMod of R
for A being Subset of V st not R is degenerated holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) by VECTSP_6:14;