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

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