let R be Ring; :: thesis: 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 )
let V be LeftMod of R; :: thesis: 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 )
let A be Subset of V; :: thesis: ( not R is degenerated implies ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) )
assume not R is degenerated ; :: thesis: ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
then 0. R <> 1. R ;
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