defpred S_{1}[ 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 S_{1}[x,y]

A2: dom f = [#] W and

A3: for x being object st x in [#] W holds

S_{1}[x,f . x]
from CLASSES1:sch 1(A1);

A4: rng f c= [#] F

ex T being finite Subset of W st

for w being Element of W st not w in T holds

f . w = 0. F

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}))

( $1 = w & $2 = Sum (l .: (T " {w})) );

A1: for x being object st x in [#] W holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in [#] W implies ex y being object st S_{1}[x,y] )

assume x in [#] W ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider x = x as Element of W ;

take Sum (l .: (T " {x})) ; :: thesis: S_{1}[x, Sum (l .: (T " {x}))]

thus S_{1}[x, Sum (l .: (T " {x}))]
; :: thesis: verum

end;assume x in [#] W ; :: thesis: ex y being object st S

then reconsider x = x as Element of W ;

take Sum (l .: (T " {x})) ; :: thesis: S

thus S

A2: dom f = [#] W and

A3: for x being object st x in [#] W holds

S

A4: rng f c= [#] F

proof

A7:
for w being Element of W holds f . w = Sum (l .: (T " {w}))
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;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

proof

reconsider f = f as Element of Funcs (([#] W),([#] F)) by A2, A4, FUNCT_2:def 2;
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;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

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

then reconsider f = f as Linear_Combination of W by VECTSP_6:def 1;
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

set C = Carrier l;

reconsider TC = T .: (Carrier l) as Subset of W ;

X c= TC

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;{ w where w is Element of W : f . w <> 0. F } c= [#] W

proof

then reconsider X = { w where w is Element of W : f . w <> 0. F } as Subset of W ;
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;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

set C = Carrier l;

reconsider TC = T .: (Carrier l) as Subset of W ;

X c= TC

proof

then reconsider X = X as finite Subset of W ;
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

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;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

then consider y being object such that
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

end;then A11: l .: (T " {w}) c= {(0. F)} by Th28;

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

proof
end;

hence
contradiction
by A7, A9; :: thesis: verumper cases
( l .: (T " {w}) = {} F or l .: (T " {w}) <> {} F )
;

end;

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

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

then l .: (T " {w}) = {(0. F)} by A13;

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

end;proof

l .: (T " {w}) c= {(0. F)}
by A10, Th28;
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;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

then l .: (T " {w}) = {(0. F)} by A13;

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

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

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

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

hence
for w being Element of W holds f . w = Sum (l .: (T " {w}))
; :: thesis: verum
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;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