set A1 = { (Sum l) where l is Linear_Combination of A : verum } ;
reconsider l = ZeroLC V as Linear_Combination of A by Th26;
{ (Sum l) where l is Linear_Combination of A : verum } c= the carrier of V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Sum l) where l is Linear_Combination of A : verum } or x in the carrier of V )
assume x in { (Sum l) where l is Linear_Combination of A : verum } ; :: thesis: x in the carrier of V
then ex l being Linear_Combination of A st x = Sum l ;
hence x in the carrier of V ; :: thesis: verum

end;

then reconsider A1 = { (Sum l) where l is Linear_Combination of A : verum } as Subset of V ;
A1: A1 is linearly-closed

proof

thus for v, u being Vector of V st v in A1 & u in A1 holds
v + u in A1 :: according to RMOD_2:def 1 :: thesis: for b₁ being Element of the carrier of R
for b₂ being Element of the carrier of V holds
( not b₂ in A1 or b₂ * b₁ in A1 )

proof

let v, u be Vector of V; :: thesis: ( v in A1 & u in A1 implies v + u in A1 )
assume that
A2: v in A1 and
A3: u in A1 ; :: thesis: v + u in A1
consider l1 being Linear_Combination of A such that
A4: v = Sum l1 by A2;
consider l2 being Linear_Combination of A such that
A5: u = Sum l2 by A3;
reconsider f = l1 + l2 as Linear_Combination of A by Th52;
v + u = Sum f by A4, A5, Th77;
hence v + u in A1 ; :: thesis: verum

end;

let a be Scalar of R; :: thesis: for b₁ being Element of the carrier of V holds
( not b₁ in A1 or b₁ * a in A1 )
let v be Vector of V; :: thesis: ( not v in A1 or v * a in A1 )
assume v in A1 ; :: thesis: v * a in A1
then consider l being Linear_Combination of A such that
A6: v = Sum l ;
reconsider f = l * a as Linear_Combination of A by Th61;
v * a = Sum f by A6, Th78;
hence v * a in A1 ; :: thesis: verum

end;

Sum l = 0. V by Lm3;
then 0. V in A1 ;
hence ex b₁ being strict Submodule of V st the carrier of b₁ = { (Sum l) where l is Linear_Combination of A : verum } by A1, RMOD_2:42; :: thesis: verum