defpred S1[ object , object ] means ex w being Element of W st
( $1 = w & $2 = Sum (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 (l .: (T " {x})) ; :: thesis: S1[x, Sum (l .: (T " {x}))]
thus S1[x, Sum (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 CLASSES1:sch 1(A1);
 A4: rng f c= [#] F
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in [#] F )
assume y in rng f ; :: thesis: y in [#] F
then consider x being object such that
A5: x in dom f and
A6: f . x = y by FUNCT_1:def 3;
ex w being Element of W st
( x = w & f . x = Sum (l .: (T " {w})) ) by A2, A3, A5;
hence y in [#] F by A6; :: thesis: verum
end;
A7: 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}))
ex w9 being Element of W st
( w = w9 & f . w = Sum (l .: (T " {w9})) ) by A3;
hence f . w = Sum (l .: (T " {w})) ; :: thesis: verum
end;
reconsider f = f as Element of Funcs (([#] W),([#] F)) by A2, 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 X = { w where w is Element of W : f . w <> 0. F } ;
{ w where w is Element of W : f . w <> 0. F } 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. F } or x in [#] W )
assume x in { w where w is Element of W : f . w <> 0. F } ; :: thesis: x in [#] W
then ex w being Element of W st
( x = w & f . w <> 0. F ) ;
hence x in [#] W ; :: thesis: verum
end;
then reconsider X = { w where w is Element of W : f . w <> 0. F } as Subset of W ;
set C = Carrier l;
reconsider TC = T .: (Carrier l) as Subset of W ;
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
A8: x = w and
A9: f . w <> 0. F ;
T " {w} meets Carrier l
proof
assume A10: T " {w} misses Carrier l ; :: thesis: contradiction
then A11: 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:8; :: thesis: verum
end;
suppose A12: l .: (T " {w}) <> {} F ; :: thesis: Sum (l .: (T " {w})) = 0. F
A13: {(0. F)} c= l .: (T " {w})
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {(0. F)} or y in l .: (T " {w}) )
assume y in {(0. F)} ; :: thesis: y in l .: (T " {w})
then A14: y = 0. F by TARSKI:def 1;
ex z being object st z in l .: (T " {w}) by A12, XBOOLE_0:def 1;
hence y in l .: (T " {w}) by A11, A14, TARSKI:def 1; :: thesis: verum
end;
l .: (T " {w}) c= {(0. F)} by A10, Th28;
then l .: (T " {w}) = {(0. F)} by A13;
hence Sum (l .: (T " {w})) = 0. F by RLVECT_2:9; :: thesis: verum
end;
end;
end;
hence contradiction by A7, A9; :: thesis: verum
end;
then consider y being object such that
A15: y in T " {w} and
A16: y in Carrier l by XBOOLE_0:3;
A17: dom T = [#] V by Th7;
reconsider y = y as Element of V by A16;
T . y in {w} by A15, FUNCT_1:def 7;
then T . y = w by TARSKI:def 1;
hence x in TC by A8, A16, A17, FUNCT_1:def 6; :: 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 1;
take f ; :: thesis: for w being Element of W holds f . w = Sum (l .: (T " {w}))
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}))
ex w9 being Element of W st
( w = w9 & f . w = Sum (l .: (T " {w9})) ) by A3;
hence f . w = Sum (l .: (T " {w})) ; :: thesis: verum
end;
hence for w being Element of W holds f . w = Sum (l .: (T " {w})) ; :: thesis: verum