defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in [#] W implies ex y being object st S1[x,y] )
assume x in [#] W ; :: thesis: ex y being object st S1[x,y]
then reconsider x = x as Element of W ;
take Sum (lCFST (l,T,x)) ; :: thesis: S1[x, Sum (lCFST (l,T,x))]
thus S1[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
S1[x,f . x] from 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 ;
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 .: () 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 ;
then T . y = w by TARSKI:def 1;
hence x in TC by ; :: 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 .: () & ( 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 .: () & ( for w being Element of W holds f . w = Sum (lCFST (l,T,w)) ) ) by A9; :: thesis: verum