set A1 = { (Sum l) where l is Linear_Combination of A : verum } ;

{ (Sum l) where l is Linear_Combination of A : verum } c= the carrier of V

reconsider l = ZeroLC V as Linear_Combination of A by RLVECT_2:22;

A1: A1 is linearly-closed

then 0. V in A1 ;

hence ex b_{1} being strict Subspace of V st the carrier of b_{1} = { (Sum l) where l is Linear_Combination of A : verum }
by A1, RLSUB_1:35; :: thesis: verum

{ (Sum l) where l is Linear_Combination of A : verum } c= the carrier of V

proof

then reconsider A1 = { (Sum l) where l is Linear_Combination of A : verum } as Subset of V ;
let x be object ; :: 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;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

reconsider l = ZeroLC V as Linear_Combination of A by RLVECT_2:22;

A1: A1 is linearly-closed

proof

Sum l = 0. V
by RLVECT_2:30;
thus
for v, u being VECTOR of V st v in A1 & u in A1 holds

v + u in A1 :: according to RLSUB_1:def 1 :: thesis: for b_{1} being object

for b_{2} being Element of the carrier of V holds

( not b_{2} in A1 or b_{1} * b_{2} in A1 )_{1} being Element of the carrier of V holds

( not b_{1} in A1 or a * b_{1} in A1 )

let v be VECTOR of V; :: thesis: ( not v in A1 or a * v in A1 )

assume v in A1 ; :: thesis: a * v in A1

then consider l being Linear_Combination of A such that

A6: v = Sum l ;

reconsider f = a * l as Linear_Combination of A by RLVECT_2:44;

a * v = Sum f by A6, Th2;

hence a * v in A1 ; :: thesis: verum

end;v + u in A1 :: according to RLSUB_1:def 1 :: thesis: for b

for b

( not b

proof

let a be Real; :: thesis: for b
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 RLVECT_2:38;

v + u = Sum f by A4, A5, Th1;

hence v + u in A1 ; :: thesis: verum

end;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 RLVECT_2:38;

v + u = Sum f by A4, A5, Th1;

hence v + u in A1 ; :: thesis: verum

( not b

let v be VECTOR of V; :: thesis: ( not v in A1 or a * v in A1 )

assume v in A1 ; :: thesis: a * v in A1

then consider l being Linear_Combination of A such that

A6: v = Sum l ;

reconsider f = a * l as Linear_Combination of A by RLVECT_2:44;

a * v = Sum f by A6, Th2;

hence a * v in A1 ; :: thesis: verum

then 0. V in A1 ;

hence ex b