theorem :: ZMODUL02:18

for V being Z_Module
for A being Subset of V holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )