let n, k be Nat; :: thesis: for X being set

for F being Function of (the_subsets_of_card (n,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

let X be set ; :: thesis: for F being Function of (the_subsets_of_card (n,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

defpred S_{1}[ Nat] means for k being Nat

for X being set

for F being Function of (the_subsets_of_card ($1,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ($1,H)) is constant );

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A143, A1);

hence for F being Function of (the_subsets_of_card (n,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) ; :: thesis: verum

for F being Function of (the_subsets_of_card (n,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

let X be set ; :: thesis: for F being Function of (the_subsets_of_card (n,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

defpred S

for X being set

for F being Function of (the_subsets_of_card ($1,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ($1,H)) is constant );

A1: for n being Nat st S

S

proof

A143:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;assume A2: S

now :: thesis: for k being Nat

for X being set

for F being Function of (the_subsets_of_card ((n + 1),X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

hence
Sfor X being set

for F being Function of (the_subsets_of_card ((n + 1),X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

let k be Nat; :: thesis: for X being set

for F being Function of (the_subsets_of_card ((n + 1),X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

let X be set ; :: thesis: for F being Function of (the_subsets_of_card ((n + 1),X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

let F be Function of (the_subsets_of_card ((n + 1),X)),k; :: thesis: ( card X = omega & X c= omega & k <> 0 implies ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) )

assume A3: card X = omega ; :: thesis: ( X c= omega & k <> 0 implies ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) )

X c= X ;

then A4: X in the_subsets_of_card (omega,X) by A3;

then reconsider A = the_subsets_of_card (omega,X) as non empty set ;

reconsider X0 = X as Element of A by A4;

defpred S_{2}[ set , set , set , set , set ] means for x1, x2 being Element of A

for y1, y2 being Element of omega st $2 = x1 & $3 = y1 & $4 = x2 & $5 = y2 holds

( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies ( x2 = X & y2 = 0 ) ) );

set Y0 = min* X;

assume A5: X c= omega ; :: thesis: ( k <> 0 implies ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) )

assume A6: k <> 0 ; :: thesis: ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

A7: for Y being set

for a being Element of Y st card Y = omega & Y c= X holds

ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

for x99 being Element of A

for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S_{2}[a,x99,y99,x199,y199]

A41: ( S . 0 = X0 & a . 0 = min* X & ( for i being Nat holds S_{2}[i,S . i,a . i,S . (i + 1),a . (i + 1)] ) )
from RECDEF_2:sch 3(A19);

defpred S_{3}[ Nat] means ( a . $1 in Segm (a . ($1 + 1)) & S . ($1 + 1) c= S . $1 & a . $1 in S . $1 & a . ($1 + 1) in S . ($1 + 1) & not a . $1 in S . ($1 + 1) );

A42: S_{3}[ 0 ]
_{4}[ object , object ] means for Y being set

for i being Element of NAT

for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = $1 & Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

ex l being Nat st

( l = $2 & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} );

defpred S_{5}[ Nat] means for i, j being Nat st i >= j & i = $1 + j holds

( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) );

A44: for i being Nat st S_{3}[i] holds

S_{3}[i + 1]
_{3}[i]
from NAT_1:sch 2(A42, A44);

A48: for l being Nat st S_{5}[l] holds

S_{5}[l + 1]
_{5}[ 0 ]
;

A59: for l being Nat holds S_{5}[l]
from NAT_1:sch 2(A58, A48);

A60: for i, j being Nat st i >= j holds

( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) )

for Y being set

for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )

x1 = x2

A85: NAT = dom a by FUNCT_2:def 1;

A86: for i being Element of NAT holds card { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } = omega

ex y being object st

( y in k & S_{4}[x,y] )

A108: for x being object st x in NAT holds

S_{4}[x,g . x]
from FUNCT_2:sch 1(A95);

g in Funcs (NAT,k) by A6, FUNCT_2:8;

then ex g9 being Function st

( g = g9 & dom g9 = NAT & rng g9 c= k ) by FUNCT_2:def 2;

then consider k9 being object such that

k9 in rng g and

A109: g " {k9} is infinite by CARD_2:101;

set H = a .: (g " {k9});

g " {k9} c= dom g by RELAT_1:132;

then g " {k9},a .: (g " {k9}) are_equipotent by A84, A85, CARD_1:33, XBOOLE_1:1;

then A110: card (g " {k9}) = card (a .: (g " {k9})) by CARD_1:5;

take H = H; :: thesis: ( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

thus H is infinite by A109, A110; :: thesis: F | (the_subsets_of_card ((n + 1),H)) is constant

A113: for y being set st y in dom (F | (the_subsets_of_card ((n + 1),H))) holds

(F | (the_subsets_of_card ((n + 1),H))) . y = k9

(F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y

end;for F being Function of (the_subsets_of_card ((n + 1),X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

let X be set ; :: thesis: for F being Function of (the_subsets_of_card ((n + 1),X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

let F be Function of (the_subsets_of_card ((n + 1),X)),k; :: thesis: ( card X = omega & X c= omega & k <> 0 implies ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) )

assume A3: card X = omega ; :: thesis: ( X c= omega & k <> 0 implies ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) )

X c= X ;

then A4: X in the_subsets_of_card (omega,X) by A3;

then reconsider A = the_subsets_of_card (omega,X) as non empty set ;

reconsider X0 = X as Element of A by A4;

defpred S

for y1, y2 being Element of omega st $2 = x1 & $3 = y1 & $4 = x2 & $5 = y2 holds

( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies ( x2 = X & y2 = 0 ) ) );

set Y0 = min* X;

assume A5: X c= omega ; :: thesis: ( k <> 0 implies ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) )

assume A6: k <> 0 ; :: thesis: ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

A7: for Y being set

for a being Element of Y st card Y = omega & Y c= X holds

ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

proof

A19:
for a being Nat
let Y be set ; :: thesis: for a being Element of Y st card Y = omega & Y c= X holds

ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

let a be Element of Y; :: thesis: ( card Y = omega & Y c= X implies ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) )

set Y1 = the_subsets_of_card (n,(Y \ {a}));

assume A8: card Y = omega ; :: thesis: ( not Y c= X or ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) )

then A9: Y is infinite ;

then reconsider Y1 = the_subsets_of_card (n,(Y \ {a})) as non empty set ;

deffunc H_{1}( Element of Y1) -> set = F . ($1 \/ {a});

assume A10: Y c= X ; :: thesis: ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

not Y is empty by A8;

then A11: {a} c= Y by ZFMISC_1:31;

A12: for x being Element of Y1 holds H_{1}(x) in k

A16: for x being Element of Y1 holds Fa . x = H_{1}(x)
from FUNCT_2:sch 8(A12);

reconsider Fa = Fa as Function of (the_subsets_of_card (n,(Y \ {a}))),k ;

A17: Y c= omega by A5, A10;

then card (Y \ {a}) = omega by A9, Th2, XBOOLE_1:1;

then consider Ha being Subset of (Y \ {a}) such that

A18: ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant ) by A2, A6, A17, XBOOLE_1:1;

take Fa ; :: thesis: ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

take Ha ; :: thesis: ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

thus ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant ) by A18; :: thesis: for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a})

let Y9 be Element of the_subsets_of_card (n,(Y \ {a})); :: thesis: Fa . Y9 = F . (Y9 \/ {a})

thus Fa . Y9 = F . (Y9 \/ {a}) by A16; :: thesis: verum

end;ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

let a be Element of Y; :: thesis: ( card Y = omega & Y c= X implies ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) )

set Y1 = the_subsets_of_card (n,(Y \ {a}));

assume A8: card Y = omega ; :: thesis: ( not Y c= X or ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) )

then A9: Y is infinite ;

then reconsider Y1 = the_subsets_of_card (n,(Y \ {a})) as non empty set ;

deffunc H

assume A10: Y c= X ; :: thesis: ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

not Y is empty by A8;

then A11: {a} c= Y by ZFMISC_1:31;

A12: for x being Element of Y1 holds H

proof

consider Fa being Function of Y1,k such that
let x be Element of Y1; :: thesis: H_{1}(x) in k

x in Y1 ;

then consider x9 being Subset of (Y \ {a}) such that

A13: x = x9 and

A14: card x9 = n ;

x \/ {a} c= (Y \ {a}) \/ {a} by A13, XBOOLE_1:9;

then x \/ {a} c= Y \/ {a} by XBOOLE_1:39;

then reconsider y = x \/ {a} as Subset of Y by A11, XBOOLE_1:12;

reconsider x99 = x9 as finite set by A14;

not a in x99

then A15: x \/ {a} in the_subsets_of_card ((n + 1),Y) ;

the_subsets_of_card ((n + 1),Y) c= the_subsets_of_card ((n + 1),X) by A10, Lm1;

hence H_{1}(x) in k
by A6, A15, FUNCT_2:5; :: thesis: verum

end;x in Y1 ;

then consider x9 being Subset of (Y \ {a}) such that

A13: x = x9 and

A14: card x9 = n ;

x \/ {a} c= (Y \ {a}) \/ {a} by A13, XBOOLE_1:9;

then x \/ {a} c= Y \/ {a} by XBOOLE_1:39;

then reconsider y = x \/ {a} as Subset of Y by A11, XBOOLE_1:12;

reconsider x99 = x9 as finite set by A14;

not a in x99

proof

then
card y = n + 1
by A13, A14, CARD_2:41;
assume
a in x99
; :: thesis: contradiction

then not a in {a} by XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then not a in {a} by XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

then A15: x \/ {a} in the_subsets_of_card ((n + 1),Y) ;

the_subsets_of_card ((n + 1),Y) c= the_subsets_of_card ((n + 1),X) by A10, Lm1;

hence H

A16: for x being Element of Y1 holds Fa . x = H

reconsider Fa = Fa as Function of (the_subsets_of_card (n,(Y \ {a}))),k ;

A17: Y c= omega by A5, A10;

then card (Y \ {a}) = omega by A9, Th2, XBOOLE_1:1;

then consider Ha being Subset of (Y \ {a}) such that

A18: ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant ) by A2, A6, A17, XBOOLE_1:1;

take Fa ; :: thesis: ex Ha being Subset of (Y \ {a}) st

( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

take Ha ; :: thesis: ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

thus ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant ) by A18; :: thesis: for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a})

let Y9 be Element of the_subsets_of_card (n,(Y \ {a})); :: thesis: Fa . Y9 = F . (Y9 \/ {a})

thus Fa . Y9 = F . (Y9 \/ {a}) by A16; :: thesis: verum

for x99 being Element of A

for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S

proof

consider S being sequence of A, a being sequence of omega such that
let a be Nat; :: thesis: for x99 being Element of A

for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S_{2}[a,x99,y99,x199,y199]

let x99 be Element of A; :: thesis: for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S_{2}[a,x99,y99,x199,y199]

let y99 be Element of omega ; :: thesis: ex x199 being Element of A ex y199 being Element of omega st S_{2}[a,x99,y99,x199,y199]

end;for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S

let x99 be Element of A; :: thesis: for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S

let y99 be Element of omega ; :: thesis: ex x199 being Element of A ex y199 being Element of omega st S

per cases
( y99 in x99 or not y99 in x99 )
;

end;

suppose A20:
y99 in x99
; :: thesis: ex x199 being Element of A ex y199 being Element of omega st S_{2}[a,x99,y99,x199,y199]

then reconsider a9 = y99 as Element of x99 ;

A21: x99 in A ;

then ex x999 being Subset of X st

( x999 = x99 & card x999 = omega ) ;

then consider Fa being Function of (the_subsets_of_card (n,(x99 \ {a9}))),k, Ha being Subset of (x99 \ {a9}) such that

A22: Ha is infinite and

A23: Fa | (the_subsets_of_card (n,Ha)) is constant and

A24: for Y9 being Element of the_subsets_of_card (n,(x99 \ {a9})) holds Fa . Y9 = F . (Y9 \/ {a9}) by A7;

Ha c= x99 by XBOOLE_1:1;

then A25: Ha c= X by A21, XBOOLE_1:1;

then card Ha = omega by A5, A22, Th2, XBOOLE_1:1;

then Ha in A by A25;

then reconsider x199 = Ha as Element of A ;

set y199 = min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ;

take x199 ; :: thesis: ex y199 being Element of omega st S_{2}[a,x99,y99,x199,y199]

take min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; :: thesis: S_{2}[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ]

A26: Ha c= omega by A5, A25;

_{2}[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ]
; :: thesis: verum

end;A21: x99 in A ;

then ex x999 being Subset of X st

( x999 = x99 & card x999 = omega ) ;

then consider Fa being Function of (the_subsets_of_card (n,(x99 \ {a9}))),k, Ha being Subset of (x99 \ {a9}) such that

A22: Ha is infinite and

A23: Fa | (the_subsets_of_card (n,Ha)) is constant and

A24: for Y9 being Element of the_subsets_of_card (n,(x99 \ {a9})) holds Fa . Y9 = F . (Y9 \/ {a9}) by A7;

Ha c= x99 by XBOOLE_1:1;

then A25: Ha c= X by A21, XBOOLE_1:1;

then card Ha = omega by A5, A22, Th2, XBOOLE_1:1;

then Ha in A by A25;

then reconsider x199 = Ha as Element of A ;

set y199 = min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ;

take x199 ; :: thesis: ex y199 being Element of omega st S

take min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; :: thesis: S

A26: Ha c= omega by A5, A25;

now :: thesis: for x1, x2 being Element of A

for y1, y2 being Element of omega st x99 = x1 & y99 = y1 & x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 holds

( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies S_{2}[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) )

hence
Sfor y1, y2 being Element of omega st x99 = x1 & y99 = y1 & x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 holds

( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies S

let x1, x2 be Element of A; :: thesis: for y1, y2 being Element of omega st x99 = x1 & y99 = y1 & x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 holds

( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies S_{2}[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) )

let y1, y2 be Element of omega ; :: thesis: ( x99 = x1 & y99 = y1 & x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 implies ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies S_{2}[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) ) )

assume that

A27: x99 = x1 and

A28: y99 = y1 ; :: thesis: ( x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 implies ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies S_{2}[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) ) )

assume that

A29: x199 = x2 and

A30: min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 ; :: thesis: ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies S_{2}[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) )

thus ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) :: thesis: ( not y1 in x1 implies S_{2}[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] )_{2}[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ]

hence S_{2}[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ]
by A20, A27, A28; :: thesis: verum

end;( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies S

let y1, y2 be Element of omega ; :: thesis: ( x99 = x1 & y99 = y1 & x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 implies ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies S

assume that

A27: x99 = x1 and

A28: y99 = y1 ; :: thesis: ( x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 implies ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies S

assume that

A29: x199 = x2 and

A30: min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 ; :: thesis: ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) & ( not y1 in x1 implies S

thus ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) :: thesis: ( not y1 in x1 implies S

proof

assume
not y1 in x1
; :: thesis: S
reconsider H1 = Ha as Subset of (x1 \ {y1}) by A27, A28;

set A9 = { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ;

reconsider F1 = Fa as Function of (the_subsets_of_card (n,(x1 \ {y1}))),k by A27, A28;

assume y1 in x1 ; :: thesis: ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

take F1 ; :: thesis: ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

take H1 ; :: thesis: ( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

for x being object st x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } holds

x in NAT

thus H1 is infinite by A22; :: thesis: ( F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

thus F1 | (the_subsets_of_card (n,H1)) is constant by A23; :: thesis: ( x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

thus x2 = H1 by A29; :: thesis: ( y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

A9 <> {}

then A38: ex y299 being Element of omega st

( min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y299 & y299 > y99 & y299 in Ha ) ;

hence y2 in H1 by A30; :: thesis: ( y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

thus y1 < y2 by A28, A30, A38; :: thesis: ( ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

thus for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) by A24, A27, A28; :: thesis: for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29

let y29 be Element of omega ; :: thesis: ( y29 > y1 & y29 in H1 implies y2 <= y29 )

assume A39: y29 > y1 ; :: thesis: ( not y29 in H1 or y2 <= y29 )

assume y29 in H1 ; :: thesis: y2 <= y29

then y29 in A9 by A28, A39;

hence y2 <= y29 by A30, NAT_1:def 1; :: thesis: verum

end;set A9 = { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ;

reconsider F1 = Fa as Function of (the_subsets_of_card (n,(x1 \ {y1}))),k by A27, A28;

assume y1 in x1 ; :: thesis: ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

take F1 ; :: thesis: ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

take H1 ; :: thesis: ( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

for x being object st x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } holds

x in NAT

proof

then reconsider A9 = { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } as Subset of NAT by TARSKI:def 3;
let x be object ; :: thesis: ( x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } implies x in NAT )

assume x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; :: thesis: x in NAT

then ex x9 being Element of omega st

( x9 = x & x9 > y99 & x9 in Ha ) ;

hence x in NAT ; :: thesis: verum

end;assume x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; :: thesis: x in NAT

then ex x9 being Element of omega st

( x9 = x & x9 > y99 & x9 in Ha ) ;

hence x in NAT ; :: thesis: verum

thus H1 is infinite by A22; :: thesis: ( F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

thus F1 | (the_subsets_of_card (n,H1)) is constant by A23; :: thesis: ( x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

thus x2 = H1 by A29; :: thesis: ( y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

A9 <> {}

proof

then
min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } in A9
by NAT_1:def 1;
set A99 = { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ;

hence contradiction by A22, A35, A31, A36, TARSKI:2; :: thesis: verum

end;A31: now :: thesis: for x being object st x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } holds

x in Ha

x in Ha

let x be object ; :: thesis: ( x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } implies b_{1} in Ha )

assume A32: x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; :: thesis: b_{1} in Ha

end;assume A32: x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; :: thesis: b

now :: thesis: for x being object st x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } holds

x in Segm (y99 + 1)

then A35:
{ y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } c= Segm (y99 + 1)
;x in Segm (y99 + 1)

let x be object ; :: thesis: ( x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } implies x in Segm (y99 + 1) )

assume x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; :: thesis: x in Segm (y99 + 1)

then consider x9 being Element of omega such that

A33: x = x9 and

A34: x9 <= y99 and

x9 in Ha ;

x9 < y99 + 1 by A34, NAT_1:13;

hence x in Segm (y99 + 1) by A33, NAT_1:44; :: thesis: verum

end;assume x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; :: thesis: x in Segm (y99 + 1)

then consider x9 being Element of omega such that

A33: x = x9 and

A34: x9 <= y99 and

x9 in Ha ;

x9 < y99 + 1 by A34, NAT_1:13;

hence x in Segm (y99 + 1) by A33, NAT_1:44; :: thesis: verum

A36: now :: thesis: for x being object st x in Ha holds

x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) }

assume
A9 = {}
; :: thesis: contradictionx in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) }

let x be object ; :: thesis: ( x in Ha implies b_{1} in A9 \/ { b_{2} where y2999 is Element of omega : ( b_{2} <= y99 & b_{2} in Ha ) } )

assume A37: x in Ha ; :: thesis: b_{1} in A9 \/ { b_{2} where y2999 is Element of omega : ( b_{2} <= y99 & b_{2} in Ha ) }

then reconsider x9 = x as Element of omega by A26;

end;assume A37: x in Ha ; :: thesis: b

then reconsider x9 = x as Element of omega by A26;

per cases
( x9 <= y99 or x9 > y99 )
;

end;

suppose
x9 <= y99
; :: thesis: b_{1} in A9 \/ { b_{2} where y2999 is Element of omega : ( b_{2} <= y99 & b_{2} in Ha ) }

then
x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) }
by A37;

hence x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } by XBOOLE_0:def 3; :: thesis: verum

end;hence x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } by XBOOLE_0:def 3; :: thesis: verum

hence contradiction by A22, A35, A31, A36, TARSKI:2; :: thesis: verum

then A38: ex y299 being Element of omega st

( min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y299 & y299 > y99 & y299 in Ha ) ;

hence y2 in H1 by A30; :: thesis: ( y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

thus y1 < y2 by A28, A30, A38; :: thesis: ( ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) )

thus for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) by A24, A27, A28; :: thesis: for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29

let y29 be Element of omega ; :: thesis: ( y29 > y1 & y29 in H1 implies y2 <= y29 )

assume A39: y29 > y1 ; :: thesis: ( not y29 in H1 or y2 <= y29 )

assume y29 in H1 ; :: thesis: y2 <= y29

then y29 in A9 by A28, A39;

hence y2 <= y29 by A30, NAT_1:def 1; :: thesis: verum

hence S

suppose A40:
not y99 in x99
; :: thesis: ex x199 being Element of A ex y199 being Element of omega st S_{2}[a,x99,y99,x199,y199]

reconsider y199 = 0 as Element of omega ;

reconsider x199 = X as Element of A by A4;

take x199 ; :: thesis: ex y199 being Element of omega st S_{2}[a,x99,y99,x199,y199]

take y199 ; :: thesis: S_{2}[a,x99,y99,x199,y199]

thus S_{2}[a,x99,y99,x199,y199]
by A40; :: thesis: verum

end;reconsider x199 = X as Element of A by A4;

take x199 ; :: thesis: ex y199 being Element of omega st S

take y199 ; :: thesis: S

thus S

A41: ( S . 0 = X0 & a . 0 = min* X & ( for i being Nat holds S

defpred S

A42: S

proof

defpred S
set i = 0 ;

reconsider i = 0 as Element of NAT ;

reconsider x1 = S . i as Element of A ;

reconsider x2 = S . (i + 1) as Element of A ;

reconsider y1 = a . i as Element of omega ;

reconsider y2 = a . (i + 1) as Element of omega ;

A43: ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) by A41;

hence a . 0 in Segm (a . (0 + 1)) by A3, A5, A41, CARD_1:27, NAT_1:44, NAT_1:def 1; :: thesis: ( S . (0 + 1) c= S . 0 & a . 0 in S . 0 & a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) )

thus S . (0 + 1) c= S . 0 by A3, A5, A41, A43, CARD_1:27, NAT_1:def 1, XBOOLE_1:1; :: thesis: ( a . 0 in S . 0 & a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) )

thus a . 0 in S . 0 by A3, A5, A41, CARD_1:27, NAT_1:def 1; :: thesis: ( a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) )

thus a . (0 + 1) in S . (0 + 1) by A3, A5, A41, A43, CARD_1:27, NAT_1:def 1; :: thesis: not a . 0 in S . (0 + 1)

not y1 in x2

end;reconsider i = 0 as Element of NAT ;

reconsider x1 = S . i as Element of A ;

reconsider x2 = S . (i + 1) as Element of A ;

reconsider y1 = a . i as Element of omega ;

reconsider y2 = a . (i + 1) as Element of omega ;

A43: ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) ) by A41;

hence a . 0 in Segm (a . (0 + 1)) by A3, A5, A41, CARD_1:27, NAT_1:44, NAT_1:def 1; :: thesis: ( S . (0 + 1) c= S . 0 & a . 0 in S . 0 & a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) )

thus S . (0 + 1) c= S . 0 by A3, A5, A41, A43, CARD_1:27, NAT_1:def 1, XBOOLE_1:1; :: thesis: ( a . 0 in S . 0 & a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) )

thus a . 0 in S . 0 by A3, A5, A41, CARD_1:27, NAT_1:def 1; :: thesis: ( a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) )

thus a . (0 + 1) in S . (0 + 1) by A3, A5, A41, A43, CARD_1:27, NAT_1:def 1; :: thesis: not a . 0 in S . (0 + 1)

not y1 in x2

proof

hence
not a . 0 in S . (0 + 1)
; :: thesis: verum
assume
y1 in x2
; :: thesis: contradiction

then not y1 in {y1} by A3, A5, A41, A43, CARD_1:27, NAT_1:def 1, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then not y1 in {y1} by A3, A5, A41, A43, CARD_1:27, NAT_1:def 1, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

for i being Element of NAT

for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = $1 & Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

ex l being Nat st

( l = $2 & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} );

defpred S

( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) );

A44: for i being Nat st S

S

proof

A47:
for i being Nat holds S
let i be Nat; :: thesis: ( S_{3}[i] implies S_{3}[i + 1] )

reconsider i9 = i + 1 as Element of NAT ;

reconsider x1 = S . i9 as Element of A ;

reconsider x2 = S . (i9 + 1) as Element of A ;

reconsider y1 = a . i9 as Element of omega ;

reconsider y2 = a . (i9 + 1) as Element of omega ;

assume A45: S_{3}[i]
; :: thesis: S_{3}[i + 1]

then A46: ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) by A41;

not y1 in x2_{3}[i + 1]
by A45, A46, NAT_1:44, XBOOLE_1:1; :: thesis: verum

end;reconsider i9 = i + 1 as Element of NAT ;

reconsider x1 = S . i9 as Element of A ;

reconsider x2 = S . (i9 + 1) as Element of A ;

reconsider y1 = a . i9 as Element of omega ;

reconsider y2 = a . (i9 + 1) as Element of omega ;

assume A45: S

then A46: ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) by A41;

not y1 in x2

proof

hence
S
assume
y1 in x2
; :: thesis: contradiction

then not y1 in {y1} by A46, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then not y1 in {y1} by A46, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

A48: for l being Nat st S

S

proof

A58:
S
let l be Nat; :: thesis: ( S_{5}[l] implies S_{5}[l + 1] )

assume A49: S_{5}[l]
; :: thesis: S_{5}[l + 1]

thus S_{5}[l + 1]
:: thesis: verum

end;assume A49: S

thus S

proof

let i, j be Nat; :: thesis: ( i >= j & i = (l + 1) + j implies ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) ) )

assume A50: i >= j ; :: thesis: ( not i = (l + 1) + j or ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) ) )

set j9 = j + 1;

assume A51: i = (l + 1) + j ; :: thesis: ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) )

then A52: i = l + (j + 1) ;

A53: S . (j + 1) c= S . j by A47;

i <> j

then A54: i >= j + 1 by NAT_1:13;

then S . i c= S . (j + 1) by A49, A52;

hence S . i c= S . j by A53; :: thesis: for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj

A55: for ai, aj9 being Nat st i <> j + 1 & ai = a . i & aj9 = a . (j + 1) holds

ai > aj9 by A49, A54, A52;

thus for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj :: thesis: verum

end;ai > aj ) ) )

assume A50: i >= j ; :: thesis: ( not i = (l + 1) + j or ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) ) )

set j9 = j + 1;

assume A51: i = (l + 1) + j ; :: thesis: ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) )

then A52: i = l + (j + 1) ;

A53: S . (j + 1) c= S . j by A47;

i <> j

proof

then
i > j
by A50, XXREAL_0:1;
assume
i = j
; :: thesis: contradiction

then 0 = l + 1 by A51;

hence contradiction ; :: thesis: verum

end;then 0 = l + 1 by A51;

hence contradiction ; :: thesis: verum

then A54: i >= j + 1 by NAT_1:13;

then S . i c= S . (j + 1) by A49, A52;

hence S . i c= S . j by A53; :: thesis: for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj

A55: for ai, aj9 being Nat st i <> j + 1 & ai = a . i & aj9 = a . (j + 1) holds

ai > aj9 by A49, A54, A52;

thus for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj :: thesis: verum

proof

let ai, aj be Nat; :: thesis: ( i <> j & ai = a . i & aj = a . j implies ai > aj )

assume i <> j ; :: thesis: ( not ai = a . i or not aj = a . j or ai > aj )

assume that

A56: ai = a . i and

A57: aj = a . j ; :: thesis: ai > aj

reconsider aj9 = a . (j + 1) as Nat ;

aj in Segm aj9 by A47, A57;

then aj9 > aj by NAT_1:44;

hence ai > aj by A55, A56, XXREAL_0:2; :: thesis: verum

end;assume i <> j ; :: thesis: ( not ai = a . i or not aj = a . j or ai > aj )

assume that

A56: ai = a . i and

A57: aj = a . j ; :: thesis: ai > aj

reconsider aj9 = a . (j + 1) as Nat ;

aj in Segm aj9 by A47, A57;

then aj9 > aj by NAT_1:44;

hence ai > aj by A55, A56, XXREAL_0:2; :: thesis: verum

A59: for l being Nat holds S

A60: for i, j being Nat st i >= j holds

( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) )

proof

A63:
for i being Element of NAT
let i, j be Nat; :: thesis: ( i >= j implies ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) ) )

assume A61: i >= j ; :: thesis: ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) )

then A62: ex l being Nat st i = j + l by NAT_1:10;

hence S . i c= S . j by A59, A61; :: thesis: for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj

thus for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj by A59, A61, A62; :: thesis: verum

end;ai > aj ) ) )

assume A61: i >= j ; :: thesis: ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj ) )

then A62: ex l being Nat st i = j + l by NAT_1:10;

hence S . i c= S . j by A59, A61; :: thesis: for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj

thus for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds

ai > aj by A59, A61, A62; :: thesis: verum

for Y being set

for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )

proof

for x1, x2 being object st x1 in dom a & x2 in dom a & a . x1 = a . x2 holds
let i be Element of NAT ; :: thesis: for Y being set

for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )

let Y be set ; :: thesis: for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )

let Fi be Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k; :: thesis: ( Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) implies ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) )

assume A64: Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } ; :: thesis: ( ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) )

consider x2 being Element of A, y2 being Element of omega such that

A65: S . (i + 1) = x2 and

A66: a . (i + 1) = y2 ;

consider x1 being Element of A, y1 being Element of omega such that

A67: ( S . i = x1 & a . i = y1 ) ;

( y1 in x1 implies ( ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) & ( not y1 in x1 implies ( x2 = X & y2 = 0 ) ) ) ) by A41, A67, A65, A66;

then consider F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k, H1 being Subset of (x1 \ {y1}) such that

H1 is infinite and

A68: ( F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 ) and

A69: for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) and

for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 by A47, A67;

reconsider F1 = F1 as Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k by A67;

assume A70: for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ; :: thesis: ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )

for x19 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds F1 . x19 = Fi . x19

then A75: the_subsets_of_card (n,Y) c= the_subsets_of_card (n,(S . (i + 1))) by Lm1;

for x, y being object st x in dom (Fi | (the_subsets_of_card (n,Y))) & y in dom (Fi | (the_subsets_of_card (n,Y))) holds

(Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y

end;for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )

let Y be set ; :: thesis: for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )

let Fi be Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k; :: thesis: ( Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) implies ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) )

assume A64: Y = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > i ) } ; :: thesis: ( ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) )

consider x2 being Element of A, y2 being Element of omega such that

A65: S . (i + 1) = x2 and

A66: a . (i + 1) = y2 ;

consider x1 being Element of A, y1 being Element of omega such that

A67: ( S . i = x1 & a . i = y1 ) ;

( y1 in x1 implies ( ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st

( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 ) ) & ( not y1 in x1 implies ( x2 = X & y2 = 0 ) ) ) ) by A41, A67, A65, A66;

then consider F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k, H1 being Subset of (x1 \ {y1}) such that

H1 is infinite and

A68: ( F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 ) and

A69: for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) and

for y29 being Element of omega st y29 > y1 & y29 in H1 holds

y2 <= y29 by A47, A67;

reconsider F1 = F1 as Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k by A67;

assume A70: for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ; :: thesis: ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )

for x19 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds F1 . x19 = Fi . x19

proof

then A71:
Fi | (the_subsets_of_card (n,(S . (i + 1)))) is constant
by A65, A68, FUNCT_2:63;
let x19 be Element of the_subsets_of_card (n,((S . i) \ {(a . i)})); :: thesis: F1 . x19 = Fi . x19

thus F1 . x19 = F . (x19 \/ {(a . i)}) by A67, A69

.= Fi . x19 by A70 ; :: thesis: verum

end;thus F1 . x19 = F . (x19 \/ {(a . i)}) by A67, A69

.= Fi . x19 by A70 ; :: thesis: verum

now :: thesis: for x being object st x in Y holds

x in S . (i + 1)

hence
Y c= S . (i + 1)
; :: thesis: Fi | (the_subsets_of_card (n,Y)) is constant x in S . (i + 1)

let x be object ; :: thesis: ( x in Y implies x in S . (i + 1) )

assume x in Y ; :: thesis: x in S . (i + 1)

then ex x9 being Element of omega st

( x = x9 & ex j being Element of NAT st

( a . j = x9 & j > i ) ) by A64;

then consider j being Element of NAT such that

A72: a . j = x and

A73: j > i ;

j >= i + 1 by A73, NAT_1:13;

then A74: S . j c= S . (i + 1) by A60;

a . j in S . j by A47;

hence x in S . (i + 1) by A72, A74; :: thesis: verum

end;assume x in Y ; :: thesis: x in S . (i + 1)

then ex x9 being Element of omega st

( x = x9 & ex j being Element of NAT st

( a . j = x9 & j > i ) ) by A64;

then consider j being Element of NAT such that

A72: a . j = x and

A73: j > i ;

j >= i + 1 by A73, NAT_1:13;

then A74: S . j c= S . (i + 1) by A60;

a . j in S . j by A47;

hence x in S . (i + 1) by A72, A74; :: thesis: verum

then A75: the_subsets_of_card (n,Y) c= the_subsets_of_card (n,(S . (i + 1))) by Lm1;

for x, y being object st x in dom (Fi | (the_subsets_of_card (n,Y))) & y in dom (Fi | (the_subsets_of_card (n,Y))) holds

(Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y

proof

hence
Fi | (the_subsets_of_card (n,Y)) is constant
by FUNCT_1:def 10; :: thesis: verum
let x, y be object ; :: thesis: ( x in dom (Fi | (the_subsets_of_card (n,Y))) & y in dom (Fi | (the_subsets_of_card (n,Y))) implies (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y )

assume A76: x in dom (Fi | (the_subsets_of_card (n,Y))) ; :: thesis: ( not y in dom (Fi | (the_subsets_of_card (n,Y))) or (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y )

then A77: x in the_subsets_of_card (n,Y) ;

x in dom Fi by A76, RELAT_1:57;

then A78: x in dom (Fi | (the_subsets_of_card (n,(S . (i + 1))))) by A75, A77, RELAT_1:57;

assume A79: y in dom (Fi | (the_subsets_of_card (n,Y))) ; :: thesis: (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y

then A80: y in the_subsets_of_card (n,Y) ;

y in dom Fi by A79, RELAT_1:57;

then A81: y in dom (Fi | (the_subsets_of_card (n,(S . (i + 1))))) by A75, A80, RELAT_1:57;

thus (Fi | (the_subsets_of_card (n,Y))) . x = ((Fi | (the_subsets_of_card (n,(S . (i + 1))))) | (the_subsets_of_card (n,Y))) . x by A75, FUNCT_1:51

.= (Fi | (the_subsets_of_card (n,(S . (i + 1))))) . x by A77, FUNCT_1:49

.= (Fi | (the_subsets_of_card (n,(S . (i + 1))))) . y by A71, A78, A81, FUNCT_1:def 10

.= ((Fi | (the_subsets_of_card (n,(S . (i + 1))))) | (the_subsets_of_card (n,Y))) . y by A80, FUNCT_1:49

.= (Fi | (the_subsets_of_card (n,Y))) . y by A75, FUNCT_1:51 ; :: thesis: verum

end;assume A76: x in dom (Fi | (the_subsets_of_card (n,Y))) ; :: thesis: ( not y in dom (Fi | (the_subsets_of_card (n,Y))) or (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y )

then A77: x in the_subsets_of_card (n,Y) ;

x in dom Fi by A76, RELAT_1:57;

then A78: x in dom (Fi | (the_subsets_of_card (n,(S . (i + 1))))) by A75, A77, RELAT_1:57;

assume A79: y in dom (Fi | (the_subsets_of_card (n,Y))) ; :: thesis: (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y

then A80: y in the_subsets_of_card (n,Y) ;

y in dom Fi by A79, RELAT_1:57;

then A81: y in dom (Fi | (the_subsets_of_card (n,(S . (i + 1))))) by A75, A80, RELAT_1:57;

thus (Fi | (the_subsets_of_card (n,Y))) . x = ((Fi | (the_subsets_of_card (n,(S . (i + 1))))) | (the_subsets_of_card (n,Y))) . x by A75, FUNCT_1:51

.= (Fi | (the_subsets_of_card (n,(S . (i + 1))))) . x by A77, FUNCT_1:49

.= (Fi | (the_subsets_of_card (n,(S . (i + 1))))) . y by A71, A78, A81, FUNCT_1:def 10

.= ((Fi | (the_subsets_of_card (n,(S . (i + 1))))) | (the_subsets_of_card (n,Y))) . y by A80, FUNCT_1:49

.= (Fi | (the_subsets_of_card (n,Y))) . y by A75, FUNCT_1:51 ; :: thesis: verum

x1 = x2

proof

then A84:
a is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom a & x2 in dom a & a . x1 = a . x2 implies x1 = x2 )

assume x1 in dom a ; :: thesis: ( not x2 in dom a or not a . x1 = a . x2 or x1 = x2 )

then reconsider i1 = x1 as Element of NAT ;

assume x2 in dom a ; :: thesis: ( not a . x1 = a . x2 or x1 = x2 )

then reconsider i2 = x2 as Element of NAT ;

reconsider ai2 = a . i2 as Element of NAT ;

reconsider ai1 = a . i1 as Element of NAT ;

assume A82: a . x1 = a . x2 ; :: thesis: x1 = x2

assume A83: x1 <> x2 ; :: thesis: contradiction

end;assume x1 in dom a ; :: thesis: ( not x2 in dom a or not a . x1 = a . x2 or x1 = x2 )

then reconsider i1 = x1 as Element of NAT ;

assume x2 in dom a ; :: thesis: ( not a . x1 = a . x2 or x1 = x2 )

then reconsider i2 = x2 as Element of NAT ;

reconsider ai2 = a . i2 as Element of NAT ;

reconsider ai1 = a . i1 as Element of NAT ;

assume A82: a . x1 = a . x2 ; :: thesis: x1 = x2

assume A83: x1 <> x2 ; :: thesis: contradiction

per cases
( i1 < i2 or i1 > i2 )
by A83, XXREAL_0:1;

end;

A85: NAT = dom a by FUNCT_2:def 1;

A86: for i being Element of NAT holds card { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } = omega

proof

A95:
for x being object st x in NAT holds
let i be Element of NAT ; :: thesis: card { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } = omega

set Z = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } ;

( a . j = x9 & j > i ) } c= NAT ;

A88: dom (a | (NAT \ (Segm (i + 1)))) = (dom a) /\ (NAT \ (Segm (i + 1))) by RELAT_1:61

.= NAT /\ (NAT \ (Segm (i + 1))) by FUNCT_2:def 1

.= (NAT /\ NAT) \ (Segm (i + 1)) by XBOOLE_1:49

.= NAT \ (Segm (i + 1)) ;

for z being object holds

( z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } iff z in rng (a | (NAT \ (Segm (i + 1)))) )

( a . j = x9 & j > i ) } = rng (a | (NAT \ (Segm (i + 1)))) by TARSKI:2;

a | (NAT \ (Segm (i + 1))) is one-to-one by A84, FUNCT_1:52;

hence card { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } = omega by A88, A94, A87, Th2, CARD_1:59; :: thesis: verum

end;( a . j = x9 & j > i ) } = omega

set Z = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } ;

now :: thesis: for z being object st z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } holds

z in NAT

then A87:
{ x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } holds

z in NAT

let z be object ; :: thesis: ( z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } implies z in NAT )

assume z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } ; :: thesis: z in NAT

then ex z9 being Element of omega st

( z = z9 & ex j being Element of NAT st

( a . j = z9 & j > i ) ) ;

hence z in NAT ; :: thesis: verum

end;( a . j = x9 & j > i ) } implies z in NAT )

assume z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } ; :: thesis: z in NAT

then ex z9 being Element of omega st

( z = z9 & ex j being Element of NAT st

( a . j = z9 & j > i ) ) ;

hence z in NAT ; :: thesis: verum

( a . j = x9 & j > i ) } c= NAT ;

A88: dom (a | (NAT \ (Segm (i + 1)))) = (dom a) /\ (NAT \ (Segm (i + 1))) by RELAT_1:61

.= NAT /\ (NAT \ (Segm (i + 1))) by FUNCT_2:def 1

.= (NAT /\ NAT) \ (Segm (i + 1)) by XBOOLE_1:49

.= NAT \ (Segm (i + 1)) ;

for z being object holds

( z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } iff z in rng (a | (NAT \ (Segm (i + 1)))) )

proof

then A94:
{ x9 where x9 is Element of omega : ex j being Element of NAT st
let z be object ; :: thesis: ( z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } iff z in rng (a | (NAT \ (Segm (i + 1)))) )

( a . j = x9 & j > i ) }

then consider j being object such that

A91: j in dom (a | (NAT \ (Segm (i + 1)))) and

A92: z = (a | (NAT \ (Segm (i + 1)))) . j by FUNCT_1:def 3;

j in dom a by A91, RELAT_1:57;

then reconsider j = j as Element of NAT ;

dom (a | (NAT \ (Segm (i + 1)))) c= NAT \ (Segm (i + 1)) by RELAT_1:58;

then not j in Segm (i + 1) by A91, XBOOLE_0:def 5;

then j >= i + 1 by NAT_1:44;

then A93: j > i by NAT_1:13;

a . j = z by A91, A92, FUNCT_1:47;

hence z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } by A93; :: thesis: verum

end;( a . j = x9 & j > i ) } iff z in rng (a | (NAT \ (Segm (i + 1)))) )

hereby :: thesis: ( z in rng (a | (NAT \ (Segm (i + 1)))) implies z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } )

assume
z in rng (a | (NAT \ (Segm (i + 1))))
; :: thesis: z in { x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i ) } )

assume
z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } ; :: thesis: z in rng (a | (NAT \ (Segm (i + 1))))

then ex z9 being Element of omega st

( z = z9 & ex j being Element of NAT st

( a . j = z9 & j > i ) ) ;

then consider j being Element of NAT such that

A89: a . j = z and

A90: j > i ;

j >= i + 1 by A90, NAT_1:13;

then not j in Segm (i + 1) by NAT_1:44;

then j in NAT \ (Segm (i + 1)) by XBOOLE_0:def 5;

hence z in rng (a | (NAT \ (Segm (i + 1)))) by A85, A89, FUNCT_1:50; :: thesis: verum

end;( a . j = x9 & j > i ) } ; :: thesis: z in rng (a | (NAT \ (Segm (i + 1))))

then ex z9 being Element of omega st

( z = z9 & ex j being Element of NAT st

( a . j = z9 & j > i ) ) ;

then consider j being Element of NAT such that

A89: a . j = z and

A90: j > i ;

j >= i + 1 by A90, NAT_1:13;

then not j in Segm (i + 1) by NAT_1:44;

then j in NAT \ (Segm (i + 1)) by XBOOLE_0:def 5;

hence z in rng (a | (NAT \ (Segm (i + 1)))) by A85, A89, FUNCT_1:50; :: thesis: verum

( a . j = x9 & j > i ) }

then consider j being object such that

A91: j in dom (a | (NAT \ (Segm (i + 1)))) and

A92: z = (a | (NAT \ (Segm (i + 1)))) . j by FUNCT_1:def 3;

j in dom a by A91, RELAT_1:57;

then reconsider j = j as Element of NAT ;

dom (a | (NAT \ (Segm (i + 1)))) c= NAT \ (Segm (i + 1)) by RELAT_1:58;

then not j in Segm (i + 1) by A91, XBOOLE_0:def 5;

then j >= i + 1 by NAT_1:44;

then A93: j > i by NAT_1:13;

a . j = z by A91, A92, FUNCT_1:47;

hence z in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } by A93; :: thesis: verum

( a . j = x9 & j > i ) } = rng (a | (NAT \ (Segm (i + 1)))) by TARSKI:2;

a | (NAT \ (Segm (i + 1))) is one-to-one by A84, FUNCT_1:52;

hence card { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } = omega by A88, A94, A87, Th2, CARD_1:59; :: thesis: verum

ex y being object st

( y in k & S

proof

consider g being sequence of k such that
let x be object ; :: thesis: ( x in NAT implies ex y being object st

( y in k & S_{4}[x,y] ) )

assume x in NAT ; :: thesis: ex y being object st

( y in k & S_{4}[x,y] )

then reconsider i9 = x as Element of NAT ;

set Y9 = S . i9;

A96: not a . i9 in S . (i9 + 1) by A47;

reconsider a9 = a . i9 as Element of S . i9 by A47;

set Z = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } ;

A97: S . (i9 + 1) c= S . i9 by A47;

S . i9 in A ;

then ex Y99 being Subset of X st

( Y99 = S . i9 & card Y99 = omega ) ;

then consider Fa being Function of (the_subsets_of_card (n,((S . i9) \ {a9}))),k, Ha being Subset of ((S . i9) \ {a9}) such that

Ha is infinite and

Fa | (the_subsets_of_card (n,Ha)) is constant and

A98: for Y99 being Element of the_subsets_of_card (n,((S . i9) \ {a9})) holds Fa . Y99 = F . (Y99 \/ {a9}) by A7;

A99: { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } c= S . (i9 + 1) by A63, A98;

( a . j = x9 & j > i9 ) } c= (S . i9) \ {(a . i9)} ;

then the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } ) c= the_subsets_of_card (n,((S . i9) \ {a9})) by Lm1;

then A101: Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } )) is Function of (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } )),k by A6, FUNCT_2:32;

A102: not card { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } c= card n by A86;

then not { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } is empty ;

then A103: not the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } ) is empty by A102, GROUP_10:1;

Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } )) is constant by A63, A98;

then consider y being Element of k such that

A104: rng (Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } ))) = {y} by A6, A101, A103, FUNCT_2:111;

reconsider y = y as set ;

take y ; :: thesis: ( y in k & S_{4}[x,y] )

thus y in k by A6; :: thesis: S_{4}[x,y]

for Y being set

for i being Element of NAT

for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )_{4}[x,y]
; :: thesis: verum

end;( y in k & S

assume x in NAT ; :: thesis: ex y being object st

( y in k & S

then reconsider i9 = x as Element of NAT ;

set Y9 = S . i9;

A96: not a . i9 in S . (i9 + 1) by A47;

reconsider a9 = a . i9 as Element of S . i9 by A47;

set Z = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } ;

A97: S . (i9 + 1) c= S . i9 by A47;

S . i9 in A ;

then ex Y99 being Subset of X st

( Y99 = S . i9 & card Y99 = omega ) ;

then consider Fa being Function of (the_subsets_of_card (n,((S . i9) \ {a9}))),k, Ha being Subset of ((S . i9) \ {a9}) such that

Ha is infinite and

Fa | (the_subsets_of_card (n,Ha)) is constant and

A98: for Y99 being Element of the_subsets_of_card (n,((S . i9) \ {a9})) holds Fa . Y99 = F . (Y99 \/ {a9}) by A7;

A99: { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } c= S . (i9 + 1) by A63, A98;

now :: thesis: for x being object st x in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } holds

x in (S . i9) \ {(a . i9)}

then
{ x9 where x9 is Element of omega : ex j being Element of NAT st ( a . j = x9 & j > i9 ) } holds

x in (S . i9) \ {(a . i9)}

let x be object ; :: thesis: ( x in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } implies x in (S . i9) \ {(a . i9)} )

assume x in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } ; :: thesis: x in (S . i9) \ {(a . i9)}

then A100: x in S . (i9 + 1) by A99;

then not x in {(a . i9)} by A96, TARSKI:def 1;

hence x in (S . i9) \ {(a . i9)} by A97, A100, XBOOLE_0:def 5; :: thesis: verum

end;( a . j = x9 & j > i9 ) } implies x in (S . i9) \ {(a . i9)} )

assume x in { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } ; :: thesis: x in (S . i9) \ {(a . i9)}

then A100: x in S . (i9 + 1) by A99;

then not x in {(a . i9)} by A96, TARSKI:def 1;

hence x in (S . i9) \ {(a . i9)} by A97, A100, XBOOLE_0:def 5; :: thesis: verum

( a . j = x9 & j > i9 ) } c= (S . i9) \ {(a . i9)} ;

then the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } ) c= the_subsets_of_card (n,((S . i9) \ {a9})) by Lm1;

then A101: Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } )) is Function of (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } )),k by A6, FUNCT_2:32;

A102: not card { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } c= card n by A86;

then not { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } is empty ;

then A103: not the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } ) is empty by A102, GROUP_10:1;

Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } )) is constant by A63, A98;

then consider y being Element of k such that

A104: rng (Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i9 ) } ))) = {y} by A6, A101, A103, FUNCT_2:111;

reconsider y = y as set ;

take y ; :: thesis: ( y in k & S

thus y in k by A6; :: thesis: S

for Y being set

for i being Element of NAT

for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

proof

hence
S
reconsider k9 = k as Element of NAT by ORDINAL1:def 12;

let Y be set ; :: thesis: for i being Element of NAT

for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

let i be Element of NAT ; :: thesis: for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

let Fi be Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k; :: thesis: ( i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) implies ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) )

assume A105: i = x ; :: thesis: ( not Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } or ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) )

k9 is Subset of NAT by STIRL2_1:8;

then reconsider l = y as Nat ;

assume A106: Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } ; :: thesis: ( ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) )

assume A107: for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ; :: thesis: ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

take l ; :: thesis: ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

thus l = y ; :: thesis: ( l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

thus l in k by A6; :: thesis: rng (Fi | (the_subsets_of_card (n,Y))) = {l}

for x19 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fa . x19 = Fi . x19

end;let Y be set ; :: thesis: for i being Element of NAT

for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

let i be Element of NAT ; :: thesis: for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds

ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

let Fi be Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k; :: thesis: ( i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } & ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) implies ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) )

assume A105: i = x ; :: thesis: ( not Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } or ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) )

k9 is Subset of NAT by STIRL2_1:8;

then reconsider l = y as Nat ;

assume A106: Y = { x9 where x9 is Element of omega : ex j being Element of NAT st

( a . j = x9 & j > i ) } ; :: thesis: ( ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) )

assume A107: for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ; :: thesis: ex l being Nat st

( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

take l ; :: thesis: ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

thus l = y ; :: thesis: ( l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

thus l in k by A6; :: thesis: rng (Fi | (the_subsets_of_card (n,Y))) = {l}

for x19 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fa . x19 = Fi . x19

proof

hence
rng (Fi | (the_subsets_of_card (n,Y))) = {l}
by A104, A105, A106, FUNCT_2:63; :: thesis: verum
let x19 be Element of the_subsets_of_card (n,((S . i) \ {(a . i)})); :: thesis: Fa . x19 = Fi . x19

thus Fa . x19 = F . (x19 \/ {(a . i)}) by A98, A105

.= Fi . x19 by A107 ; :: thesis: verum

end;thus Fa . x19 = F . (x19 \/ {(a . i)}) by A98, A105

.= Fi . x19 by A107 ; :: thesis: verum

A108: for x being object st x in NAT holds

S

g in Funcs (NAT,k) by A6, FUNCT_2:8;

then ex g9 being Function st

( g = g9 & dom g9 = NAT & rng g9 c= k ) by FUNCT_2:def 2;

then consider k9 being object such that

k9 in rng g and

A109: g " {k9} is infinite by CARD_2:101;

set H = a .: (g " {k9});

g " {k9} c= dom g by RELAT_1:132;

then g " {k9},a .: (g " {k9}) are_equipotent by A84, A85, CARD_1:33, XBOOLE_1:1;

then A110: card (g " {k9}) = card (a .: (g " {k9})) by CARD_1:5;

now :: thesis: for y being object st y in a .: (g " {k9}) holds

y in X

then reconsider H = a .: (g " {k9}) as Subset of X by TARSKI:def 3;y in X

let y be object ; :: thesis: ( y in a .: (g " {k9}) implies y in X )

assume y in a .: (g " {k9}) ; :: thesis: y in X

then consider x being object such that

A111: [x,y] in a and

x in g " {k9} by RELAT_1:def 13;

x in dom a by A111, FUNCT_1:1;

then reconsider i = x as Element of NAT ;

y = a . x by A111, FUNCT_1:1;

then A112: y in S . i by A47;

S . i in the_subsets_of_card (omega,X) ;

hence y in X by A112; :: thesis: verum

end;assume y in a .: (g " {k9}) ; :: thesis: y in X

then consider x being object such that

A111: [x,y] in a and

x in g " {k9} by RELAT_1:def 13;

x in dom a by A111, FUNCT_1:1;

then reconsider i = x as Element of NAT ;

y = a . x by A111, FUNCT_1:1;

then A112: y in S . i by A47;

S . i in the_subsets_of_card (omega,X) ;

hence y in X by A112; :: thesis: verum

take H = H; :: thesis: ( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

thus H is infinite by A109, A110; :: thesis: F | (the_subsets_of_card ((n + 1),H)) is constant

A113: for y being set st y in dom (F | (the_subsets_of_card ((n + 1),H))) holds

(F | (the_subsets_of_card ((n + 1),H))) . y = k9

proof

for x, y being object st x in dom (F | (the_subsets_of_card ((n + 1),H))) & y in dom (F | (the_subsets_of_card ((n + 1),H))) holds
let y be set ; :: thesis: ( y in dom (F | (the_subsets_of_card ((n + 1),H))) implies (F | (the_subsets_of_card ((n + 1),H))) . y = k9 )

assume y in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis: (F | (the_subsets_of_card ((n + 1),H))) . y = k9

then A114: y in the_subsets_of_card ((n + 1),H) by RELAT_1:57;

then consider Y being Subset of H such that

A115: y = Y and

A116: card Y = n + 1 ;

set y0 = min* Y;

set Y9 = y \ {(min* Y)};

Y c= X by XBOOLE_1:1;

then A117: Y c= NAT by A5;

then A118: min* Y in Y by A116, CARD_1:27, NAT_1:def 1;

then consider x0 being object such that

x0 in dom a and

A119: x0 in g " {k9} and

A120: min* Y = a . x0 by FUNCT_1:def 6;

consider y09 being object such that

y09 in rng g and

A121: [x0,y09] in g and

A122: y09 in {k9} by A119, RELAT_1:131;

A123: x0 in dom g by A121, FUNCT_1:1;

A124: g . x0 = y09 by A121, FUNCT_1:1;

reconsider x0 = x0 as Element of NAT by A123;

set Y0 = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ;

{(min* Y)} c= y by A115, A118, ZFMISC_1:31;

then A125: (y \ {(min* Y)}) \/ {(a . x0)} = y by A120, XBOOLE_1:45;

reconsider a9 = a . x0 as Element of S . x0 by A47;

S . x0 in the_subsets_of_card (omega,X) ;

then ex S0 being Subset of X st

( S0 = S . x0 & card S0 = omega ) ;

then consider F0 being Function of (the_subsets_of_card (n,((S . x0) \ {a9}))),k, H0 being Subset of ((S . x0) \ {a9}) such that

H0 is infinite and

F0 | (the_subsets_of_card (n,H0)) is constant and

A126: for Y9 being Element of the_subsets_of_card (n,((S . x0) \ {a9})) holds F0 . Y9 = F . (Y9 \/ {a9}) by A7;

reconsider y9 = y as finite set by A115, A116;

card (y \ {(min* Y)}) c= card y9 by CARD_1:11;

then reconsider Y99 = y \ {(min* Y)} as finite set ;

A127: { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } c= S . (x0 + 1) by A63, A126;

( a . j = x & j > x0 ) } by TARSKI:def 3;

min* Y in {(min* Y)} by TARSKI:def 1;

then not a . x0 in y \ {(min* Y)} by A120, XBOOLE_0:def 5;

then card y9 = (card Y99) + 1 by A125, CARD_2:41;

then A136: y \ {(min* Y)} in the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ) by A115, A116, A135;

ex l being Nat st

( l = g . x0 & l in k & rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) = {l} ) by A108, A126;

then A137: rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) = {k9} by A122, A124, TARSKI:def 1;

S . (x0 + 1) c= S . x0 by A47;

then { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } c= S . x0 by A127;

then A138: { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } \ {(a . x0)} c= (S . x0) \ {(a . x0)} by XBOOLE_1:33;

not a . x0 in { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } by A47, A127;

then { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } c= (S . x0) \ {(a . x0)} by A138, ZFMISC_1:57;

then A139: the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ) c= the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by Lm1;

then A140: y \ {(min* Y)} in the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by A136;

reconsider Y9 = y \ {(min* Y)} as Element of the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by A139, A136;

Y9 in dom F0 by A6, A140, FUNCT_2:def 1;

then Y9 in dom (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) by A136, RELAT_1:57;

then (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) . Y9 in rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) by FUNCT_1:3;

then (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) . Y9 = k9 by A137, TARSKI:def 1;

then A141: F0 . Y9 = k9 by A136, FUNCT_1:49;

F0 . Y9 = F . (Y9 \/ {(a . x0)}) by A126;

hence (F | (the_subsets_of_card ((n + 1),H))) . y = k9 by A114, A125, A141, FUNCT_1:49; :: thesis: verum

end;assume y in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis: (F | (the_subsets_of_card ((n + 1),H))) . y = k9

then A114: y in the_subsets_of_card ((n + 1),H) by RELAT_1:57;

then consider Y being Subset of H such that

A115: y = Y and

A116: card Y = n + 1 ;

set y0 = min* Y;

set Y9 = y \ {(min* Y)};

Y c= X by XBOOLE_1:1;

then A117: Y c= NAT by A5;

then A118: min* Y in Y by A116, CARD_1:27, NAT_1:def 1;

then consider x0 being object such that

x0 in dom a and

A119: x0 in g " {k9} and

A120: min* Y = a . x0 by FUNCT_1:def 6;

consider y09 being object such that

y09 in rng g and

A121: [x0,y09] in g and

A122: y09 in {k9} by A119, RELAT_1:131;

A123: x0 in dom g by A121, FUNCT_1:1;

A124: g . x0 = y09 by A121, FUNCT_1:1;

reconsider x0 = x0 as Element of NAT by A123;

set Y0 = { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ;

{(min* Y)} c= y by A115, A118, ZFMISC_1:31;

then A125: (y \ {(min* Y)}) \/ {(a . x0)} = y by A120, XBOOLE_1:45;

reconsider a9 = a . x0 as Element of S . x0 by A47;

S . x0 in the_subsets_of_card (omega,X) ;

then ex S0 being Subset of X st

( S0 = S . x0 & card S0 = omega ) ;

then consider F0 being Function of (the_subsets_of_card (n,((S . x0) \ {a9}))),k, H0 being Subset of ((S . x0) \ {a9}) such that

H0 is infinite and

F0 | (the_subsets_of_card (n,H0)) is constant and

A126: for Y9 being Element of the_subsets_of_card (n,((S . x0) \ {a9})) holds F0 . Y9 = F . (Y9 \/ {a9}) by A7;

reconsider y9 = y as finite set by A115, A116;

card (y \ {(min* Y)}) c= card y9 by CARD_1:11;

then reconsider Y99 = y \ {(min* Y)} as finite set ;

A127: { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } c= S . (x0 + 1) by A63, A126;

now :: thesis: for x being object st x in y \ {(min* Y)} holds

x in { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) }

then A135:
y \ {(min* Y)} is Subset of { x where x is Element of omega : ex j being Element of NAT st x in { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) }

let x be object ; :: thesis: ( x in y \ {(min* Y)} implies x in { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } )

assume A128: x in y \ {(min* Y)} ; :: thesis: x in { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) }

then A129: x in y ;

then consider j being object such that

A130: j in dom a and

j in g " {k9} and

A131: x = a . j by A115, FUNCT_1:def 6;

reconsider x9 = x as Element of omega by A115, A117, A129;

A132: not x in {(min* Y)} by A128, XBOOLE_0:def 5;

ex j being Element of NAT st

( a . j = x9 & j > x0 )

( a . j = x & j > x0 ) } ; :: thesis: verum

end;( a . j = x & j > x0 ) } )

assume A128: x in y \ {(min* Y)} ; :: thesis: x in { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) }

then A129: x in y ;

then consider j being object such that

A130: j in dom a and

j in g " {k9} and

A131: x = a . j by A115, FUNCT_1:def 6;

reconsider x9 = x as Element of omega by A115, A117, A129;

A132: not x in {(min* Y)} by A128, XBOOLE_0:def 5;

ex j being Element of NAT st

( a . j = x9 & j > x0 )

proof

hence
x in { x where x is Element of omega : ex j being Element of NAT st
reconsider j = j as Element of NAT by A130;

take j ; :: thesis: ( a . j = x9 & j > x0 )

thus a . j = x9 by A131; :: thesis: j > x0

A133: min* Y <= x9 by A115, A117, A128, NAT_1:def 1;

thus j > x0 :: thesis: verum

end;take j ; :: thesis: ( a . j = x9 & j > x0 )

thus a . j = x9 by A131; :: thesis: j > x0

A133: min* Y <= x9 by A115, A117, A128, NAT_1:def 1;

thus j > x0 :: thesis: verum

proof

assume A134:
x0 >= j
; :: thesis: contradiction

x0 <> j by A120, A132, A131, TARSKI:def 1;

hence contradiction by A60, A120, A131, A133, A134; :: thesis: verum

end;x0 <> j by A120, A132, A131, TARSKI:def 1;

hence contradiction by A60, A120, A131, A133, A134; :: thesis: verum

( a . j = x & j > x0 ) } ; :: thesis: verum

( a . j = x & j > x0 ) } by TARSKI:def 3;

min* Y in {(min* Y)} by TARSKI:def 1;

then not a . x0 in y \ {(min* Y)} by A120, XBOOLE_0:def 5;

then card y9 = (card Y99) + 1 by A125, CARD_2:41;

then A136: y \ {(min* Y)} in the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ) by A115, A116, A135;

ex l being Nat st

( l = g . x0 & l in k & rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) = {l} ) by A108, A126;

then A137: rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) = {k9} by A122, A124, TARSKI:def 1;

S . (x0 + 1) c= S . x0 by A47;

then { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } c= S . x0 by A127;

then A138: { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } \ {(a . x0)} c= (S . x0) \ {(a . x0)} by XBOOLE_1:33;

not a . x0 in { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } by A47, A127;

then { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } c= (S . x0) \ {(a . x0)} by A138, ZFMISC_1:57;

then A139: the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ) c= the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by Lm1;

then A140: y \ {(min* Y)} in the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by A136;

reconsider Y9 = y \ {(min* Y)} as Element of the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by A139, A136;

Y9 in dom F0 by A6, A140, FUNCT_2:def 1;

then Y9 in dom (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) by A136, RELAT_1:57;

then (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) . Y9 in rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) by FUNCT_1:3;

then (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st

( a . j = x & j > x0 ) } ))) . Y9 = k9 by A137, TARSKI:def 1;

then A141: F0 . Y9 = k9 by A136, FUNCT_1:49;

F0 . Y9 = F . (Y9 \/ {(a . x0)}) by A126;

hence (F | (the_subsets_of_card ((n + 1),H))) . y = k9 by A114, A125, A141, FUNCT_1:49; :: thesis: verum

(F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y

proof

hence
F | (the_subsets_of_card ((n + 1),H)) is constant
by FUNCT_1:def 10; :: thesis: verum
let x, y be object ; :: thesis: ( x in dom (F | (the_subsets_of_card ((n + 1),H))) & y in dom (F | (the_subsets_of_card ((n + 1),H))) implies (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y )

assume x in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis: ( not y in dom (F | (the_subsets_of_card ((n + 1),H))) or (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y )

then A142: (F | (the_subsets_of_card ((n + 1),H))) . x = k9 by A113;

assume y in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis: (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y

hence (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y by A113, A142; :: thesis: verum

end;assume x in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis: ( not y in dom (F | (the_subsets_of_card ((n + 1),H))) or (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y )

then A142: (F | (the_subsets_of_card ((n + 1),H))) . x = k9 by A113;

assume y in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis: (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y

hence (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y by A113, A142; :: thesis: verum

proof

for n being Nat holds S
let k be Nat; :: thesis: for X being set

for F being Function of (the_subsets_of_card (0,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant )

let X be set ; :: thesis: for F being Function of (the_subsets_of_card (0,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant )

set H = X;

X c= X ;

then reconsider H = X as Subset of X ;

let F be Function of (the_subsets_of_card (0,X)),k; :: thesis: ( card X = omega & X c= omega & k <> 0 implies ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) )

assume A144: card X = omega ; :: thesis: ( not X c= omega or not k <> 0 or ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) )

assume X c= omega ; :: thesis: ( not k <> 0 or ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) )

assume k <> 0 ; :: thesis: ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant )

take H ; :: thesis: ( H is infinite & F | (the_subsets_of_card (0,H)) is constant )

thus H is infinite by A144; :: thesis: F | (the_subsets_of_card (0,H)) is constant

for x, y being object st x in dom (F | (the_subsets_of_card (0,H))) & y in dom (F | (the_subsets_of_card (0,H))) holds

(F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y

end;for F being Function of (the_subsets_of_card (0,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant )

let X be set ; :: thesis: for F being Function of (the_subsets_of_card (0,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant )

set H = X;

X c= X ;

then reconsider H = X as Subset of X ;

let F be Function of (the_subsets_of_card (0,X)),k; :: thesis: ( card X = omega & X c= omega & k <> 0 implies ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) )

assume A144: card X = omega ; :: thesis: ( not X c= omega or not k <> 0 or ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) )

assume X c= omega ; :: thesis: ( not k <> 0 or ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant ) )

assume k <> 0 ; :: thesis: ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (0,H)) is constant )

take H ; :: thesis: ( H is infinite & F | (the_subsets_of_card (0,H)) is constant )

thus H is infinite by A144; :: thesis: F | (the_subsets_of_card (0,H)) is constant

for x, y being object st x in dom (F | (the_subsets_of_card (0,H))) & y in dom (F | (the_subsets_of_card (0,H))) holds

(F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y

proof

hence
F | (the_subsets_of_card (0,H)) is constant
by FUNCT_1:def 10; :: thesis: verum
let x, y be object ; :: thesis: ( x in dom (F | (the_subsets_of_card (0,H))) & y in dom (F | (the_subsets_of_card (0,H))) implies (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y )

assume A145: x in dom (F | (the_subsets_of_card (0,H))) ; :: thesis: ( not y in dom (F | (the_subsets_of_card (0,H))) or (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y )

A146: dom (F | (the_subsets_of_card (0,H))) = dom (F | {0}) by Lm2

.= (dom F) /\ {0} by RELAT_1:61 ;

assume y in dom (F | (the_subsets_of_card (0,H))) ; :: thesis: (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y

then y in {0} by A146, XBOOLE_0:def 4;

then A147: y = 0 by TARSKI:def 1;

x in {0} by A146, A145, XBOOLE_0:def 4;

hence (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y by A147, TARSKI:def 1; :: thesis: verum

end;assume A145: x in dom (F | (the_subsets_of_card (0,H))) ; :: thesis: ( not y in dom (F | (the_subsets_of_card (0,H))) or (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y )

A146: dom (F | (the_subsets_of_card (0,H))) = dom (F | {0}) by Lm2

.= (dom F) /\ {0} by RELAT_1:61 ;

assume y in dom (F | (the_subsets_of_card (0,H))) ; :: thesis: (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y

then y in {0} by A146, XBOOLE_0:def 4;

then A147: y = 0 by TARSKI:def 1;

x in {0} by A146, A145, XBOOLE_0:def 4;

hence (F | (the_subsets_of_card (0,H))) . x = (F | (the_subsets_of_card (0,H))) . y by A147, TARSKI:def 1; :: thesis: verum

hence for F being Function of (the_subsets_of_card (n,X)),k st card X = omega & X c= omega & k <> 0 holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) ; :: thesis: verum