defpred S_{1}[ 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_{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= the carrier of R

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

set C = Carrier l;

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

A9: X c= TC

ex T being finite Subset of W st

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

f . w = 0. R

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

( $1 = w & $2 = Sum (lCFST (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 (lCFST (l,T,x)) ; :: thesis: S_{1}[x, Sum (lCFST (l,T,x))]

thus S_{1}[x, Sum (lCFST (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 (lCFST (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= the carrier of R

proof

A8:
for w being Element of W holds f . w = Sum (lCFST (l,T,w))
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;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

proof

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

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

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

set C = Carrier l;

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

A9: 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

A10: x = w and

A11: f . w <> 0. R ;

T " {w} meets Carrier l

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

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

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

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

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

thus for w being Element of W st not w in X holds

f . w = 0. R ; :: thesis: verum

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

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