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
proof
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;
then reconsider A1 = { (Sum l) where l is Linear_Combination of A : verum } as Subset of V ;
reconsider l = ZeroLC V as Linear_Combination of A by VECTSP_6:5;
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 VECTSP_4:def 1 :: thesis: for b1 being Element of the carrier of GF
for b2 being Element of the carrier of V holds
( not b2 in A1 or b1 * b2 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 VECTSP_6:24;
v + u = Sum f by A4, A5, VECTSP_6:44;
hence v + u in A1 ; :: thesis: verum
end;
let a be Scalar of ; :: thesis: for b1 being Element of the carrier of V holds
( not b1 in A1 or a * b1 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 VECTSP_6:31;
a * v = Sum f by A6, TH3;
hence a * v in A1 ; :: thesis: verum
end;
Sum l = 0. V by VECTSP_6:15;
then 0. V in A1 ;
hence ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } by A1, VECTSP_4:34; :: thesis: verum