let K be Ring; :: thesis:
let V be LeftMod of K; :: thesis:
let A be Subset of V; :: thesis:
let l be Linear_Combination of A; :: thesis:
assume A1: ( A <> {} & A is linearly-closed ) ; :: thesis:

now :: thesis:

per cases ;

suppose 0. K <> 1_ K ; :: thesis:

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

end;

suppose 0. K = 1_ K ; :: thesis:

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

end;

end;

end;

hence Sum l in A ; :: thesis: