defpred S₁[ object , object ] means ex w being Element of W st
( $1 = w & $2 = Sum (lCFST (l,T,w)) );
A1: for x being object st x in [#] W holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in [#] W implies ex y being object st S₁[x,y] )
assume x in [#] W ; :: thesis: ex y being object st S₁[x,y]
then reconsider x = x as Element of W ;
take Sum (lCFST (l,T,x)) ; :: thesis: S₁[x, Sum (lCFST (l,T,x))]
thus S₁[x, Sum (lCFST (l,T,x))] ; :: thesis: verum

end;

consider f being Function such that
A2: dom f = [#] W and
A3: for x being object st x in [#] W holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
A4: rng f c= the carrier of R

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of R )
assume y in rng f ; :: thesis: y in the carrier of R
then consider x being object such that
A5: x in dom f and
A6: f . x = y by FUNCT_1:def 3;
consider w being Element of W such that
A7: ( x = w & f . x = Sum (lCFST (l,T,w)) ) by A2, A3, A5;
thus y in the carrier of R by A6, A7; :: thesis: verum

end;

A8: for w being Element of W holds f . w = Sum (lCFST (l,T,w))

proof

let w be Element of W; :: thesis: f . w = Sum (lCFST (l,T,w))
ex w9 being Element of W st
( w = w9 & f . w = Sum (lCFST (l,T,w9)) ) by A3;
hence f . w = Sum (lCFST (l,T,w)) ; :: thesis: verum

end;

reconsider f = f as Element of Funcs (([#] W), the carrier of R) by A2, A4, FUNCT_2:def 2;
set X = { w where w is Element of W : f . w <> 0. R } ;
{ w where w is Element of W : f . w <> 0. R } c= [#] W

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of W : f . w <> 0. R } or x in [#] W )
assume x in { w where w is Element of W : f . w <> 0. R } ; :: thesis: x in [#] W
then ex w being Element of W st
( x = w & f . w <> 0. R ) ;
hence x in [#] W ; :: thesis: verum

end;

then reconsider X = { w where w is Element of W : f . w <> 0. R } as Subset of W ;
set C = Carrier l;
reconsider TC = T .: (Carrier l) as Subset of W ;
A9: X c= TC

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in TC )
assume x in X ; :: thesis: x in TC
then consider w being Element of W such that
A10: x = w and
A11: f . w <> 0. R ;
T " {w} meets Carrier l

proof

assume T " {w} misses Carrier l ; :: thesis: contradiction
then lCFST (l,T,w) = <*> the carrier of R ;
then Sum (lCFST (l,T,w)) = 0. R by RLVECT_1:43;
hence contradiction by A8, A11; :: thesis: verum

end;

then consider y being object such that
A13: y in T " {w} and
A14: y in Carrier l by XBOOLE_0:3;
A15: dom T = [#] V by RANKNULL:7;
reconsider y = y as Element of V by A14;
T . y in {w} by A13, FUNCT_1:def 7;
then T . y = w by TARSKI:def 1;
hence x in TC by A10, A14, A15, FUNCT_1:def 6; :: thesis: verum

end;

then reconsider X = X as finite Subset of W ;
ex T being finite Subset of W st
for w being Element of W st not w in T holds
f . w = 0. R

proof

take X ; :: thesis: for w being Element of W st not w in X holds
f . w = 0. R
thus for w being Element of W st not w in X holds
f . w = 0. R ; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of W by VECTSP_6:def 1;
take f ; :: thesis: ( Carrier f c= T .: (Carrier l) & ( for w being Element of W holds f . w = Sum (lCFST (l,T,w)) ) )
for w being Element of W holds f . w = Sum (lCFST (l,T,w))

proof

let w be Element of W; :: thesis: f . w = Sum (lCFST (l,T,w))
ex w9 being Element of W st
( w = w9 & f . w = Sum (lCFST (l,T,w9)) ) by A3;
hence f . w = Sum (lCFST (l,T,w)) ; :: thesis: verum

end;

hence ( Carrier f c= T .: (Carrier l) & ( for w being Element of W holds f . w = Sum (lCFST (l,T,w)) ) ) by A9; :: thesis: verum