let V be Z_Module; :: thesis: 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 )
let A be Subset of V; :: thesis: ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
0. INT.Ring <> 1. INT.Ring ;
then ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) by VECTSP_6:14;
hence ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) ; :: thesis: verum