let K be Ring; :: thesis: for V being LeftMod of K
for A being Subset of V
for l being Linear_Combination of A st A <> {} & A is linearly-closed holds
Sum l in A
let V be LeftMod of K; :: thesis: for A being Subset of V
for l being Linear_Combination of A st A <> {} & A is linearly-closed holds
Sum l in A
let A be Subset of V; :: thesis: for l being Linear_Combination of A st A <> {} & A is linearly-closed holds
Sum l in A
let l be Linear_Combination of A; :: thesis: ( A <> {} & A is linearly-closed implies Sum l in A )
assume A1: ( A <> {} & A is linearly-closed ) ; :: thesis: Sum l in A

now :: thesis: Sum l in A

per cases ( 0. K <> 1_ K or 0. K = 1_ K ) ;

suppose 0. K <> 1_ K ; :: thesis: Sum l in A

hence Sum l in A by A1, VECTSP_6:14; :: thesis: verum

end;

suppose 0. K = 1_ K ; :: thesis: Sum l in A

then K is trivial ;
then Sum l = 0. V by Th5;
hence Sum l in A by A1, VECTSP_4:1; :: thesis: verum

end;

end;

end;

hence Sum l in A ; :: thesis: verum