defpred S₁[ set , set ] means ex w being Element of W st
( $1 = w & $2 = Sum (l .: (T " {w})) );
A2: for x being set st x in [#] W holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in [#] W implies ex y being set st S₁[x,y] )
assume A3: x in [#] W ; :: thesis: ex y being set st S₁[x,y]
reconsider x = x as Element of W by A3;
take Sum (l .: (T " {x})) ; :: thesis: S₁[x, Sum (l .: (T " {x}))]
thus S₁[x, Sum (l .: (T " {x}))] ; :: thesis: verum

end;

consider f being Function such that
A4: dom f = [#] W and
A5: for x being set st x in [#] W holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
A6: for w being Element of W holds f . w = Sum (l .: (T " {w}))

proof

let w be Element of W; :: thesis: f . w = Sum (l .: (T " {w}))
consider w' being Element of W such that
A7: w = w' and
A8: f . w = Sum (l .: (T " {w'})) by A5;
thus f . w = Sum (l .: (T " {w})) by A7, A8; :: thesis: verum

end;

rng f c= [#] F

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in [#] F )
assume A9: y in rng f ; :: thesis: y in [#] F
consider x being set such that
A10: x in dom f and
A11: f . x = y by A9, FUNCT_1:def 5;
consider w being Element of W such that
x = w and
A12: f . x = Sum (l .: (T " {w})) by A4, A5, A10;
thus y in [#] F by A11, A12; :: thesis: verum

end;

then reconsider f = f as Element of Funcs ([#] W),([#] F) by A4, FUNCT_2:def 2;
ex T being finite Subset of W st
for w being Element of W st not w in T holds
f . w = 0. F

proof

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

proof

{ w where w is Element of W : f . w <> 0. F } c= [#] W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of W : f . w <> 0. F } or x in [#] W )
assume A13: x in { w where w is Element of W : f . w <> 0. F } ; :: thesis: x in [#] W
consider w being Element of W such that
A14: x = w and
f . w <> 0. F by A13;
thus x in [#] W by A14; :: thesis: verum

end;

hence { w where w is Element of W : f . w <> 0. F } is Subset of W ; :: thesis: verum

end;

then reconsider X = { w where w is Element of W : f . w <> 0. F } as Subset of W ;
X c= TC

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in TC )
assume A15: x in X ; :: thesis: x in TC
consider w being Element of W such that
A16: x = w and
A17: f . w <> 0. F by A15;
T " {w} meets Carrier l

proof

assume A18: T " {w} misses Carrier l ; :: thesis: contradiction
then A19: l .: (T " {w}) c= {(0. F)} by Th28;
Sum (l .: (T " {w})) = 0. F

proof

per cases ( l .: (T " {w}) = {} F or l .: (T " {w}) <> {} F ) ;

suppose l .: (T " {w}) = {} F ; :: thesis: Sum (l .: (T " {w})) = 0. F

hence Sum (l .: (T " {w})) = 0. F by RLVECT_2:14; :: thesis: verum

end;

suppose A20: l .: (T " {w}) <> {} F ; :: thesis: Sum (l .: (T " {w})) = 0. F

l .: (T " {w}) = {(0. F)}

proof

thus l .: (T " {w}) c= {(0. F)} by A18, Th28; :: according to XBOOLE_0:def 10 :: thesis: {(0. F)} c= l .: (T " {w})
thus {(0. F)} c= l .: (T " {w}) :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {(0. F)} or y in l .: (T " {w}) )
assume A21: y in {(0. F)} ; :: thesis: y in l .: (T " {w})
A22: y = 0. F by A21, TARSKI:def 1;
consider z being set such that
A23: z in l .: (T " {w}) by A20, XBOOLE_0:def 1;
thus y in l .: (T " {w}) by A19, A22, A23, TARSKI:def 1; :: thesis: verum

end;

end;

hence Sum (l .: (T " {w})) = 0. F by RLVECT_2:15; :: thesis: verum

end;

end;

end;

hence contradiction by A6, A17; :: thesis: verum

end;

then consider y being set such that
A24: y in T " {w} and
A25: y in Carrier l by XBOOLE_0:3;
reconsider y = y as Element of V by A25;
A26: dom T = [#] V by Th7;
T . y in {w} by A24, FUNCT_1:def 13;
then T . y = w by TARSKI:def 1;
hence x in TC by A16, A25, A26, FUNCT_1:def 12; :: thesis: verum

end;

then reconsider X = X as finite Subset of W ;
take X ; :: thesis: for w being Element of W st not w in X holds
f . w = 0. F
thus for w being Element of W st not w in X holds
f . w = 0. F ; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of W by VECTSP_6:def 4;
A27: for w being Element of W holds f . w = Sum (l .: (T " {w}))

proof

let w be Element of W; :: thesis: f . w = Sum (l .: (T " {w}))
consider w' being Element of W such that
A28: w = w' and
A29: f . w = Sum (l .: (T " {w'})) by A5;
thus f . w = Sum (l .: (T " {w})) by A28, A29; :: thesis: verum

end;

take f ; :: thesis: for w being Element of W holds f . w = Sum (l .: (T " {w}))
thus for w being Element of W holds f . w = Sum (l .: (T " {w})) by A27; :: thesis: verum