set X = { l where l is C_Linear_Combination of A : verum } ;
{ l where l is C_Linear_Combination of A : verum } c= the carrier of (LC_CLSpace V)

proof

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

end;

then reconsider X = { l where l is C_Linear_Combination of A : verum } as Subset of (LC_CLSpace V) ;
A1: for v, u being VECTOR of (LC_CLSpace V) st v in X & u in X holds
v + u in X

proof

let v, u be VECTOR of (LC_CLSpace V); :: thesis: ( v in X & u in X implies v + u in X )
assume that
A2: v in X and
A3: u in X ; :: thesis: v + u in X
consider l1 being C_Linear_Combination of A such that
A4: v = l1 by A2;
consider l2 being C_Linear_Combination of A such that
A5: u = l2 by A3;
A6: u = vector ((LC_CLSpace V),l2) by A5, RLVECT_2:1;
v = vector ((LC_CLSpace V),l1) by A4, RLVECT_2:1;
then v + u = l1 + l2 by A6, Th38;
hence v + u in X ; :: thesis: verum

end;

ZeroCLC V is C_Linear_Combination of A by Th4;
then A7: ZeroCLC V in X ;
for a being Complex
for v being VECTOR of (LC_CLSpace V) st v in X holds
a * v in X

proof

let a be Complex; :: thesis: for v being VECTOR of (LC_CLSpace V) st v in X holds
a * v in X
let v be VECTOR of (LC_CLSpace V); :: thesis: ( v in X implies a * v in X )
assume v in X ; :: thesis: a * v in X
then consider l being C_Linear_Combination of A such that
A8: v = l ;
a * v = a * (vector ((LC_CLSpace V),l)) by A8, RLVECT_2:1
.= a * l by Th39 ;
then a * v is C_Linear_Combination of A by Th26;
hence a * v in X ; :: thesis: verum

end;

then X is linearly-closed by A1;
hence ex b₁ being strict Subspace of LC_CLSpace V st the carrier of b₁ = { l where l is C_Linear_Combination of A : verum } by A7, CLVECT_1:54; :: thesis: verum