let n, k be Nat; :: thesis:
let X be set ; :: thesis:
defpred S₁[ 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₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:

let k be Nat; :: thesis:
let X be set ; :: thesis:
let F be Function of (the_subsets_of_card ((n + 1),X)),k; :: thesis:
assume A3: card X = omega ; :: thesis:
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₂[ 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:
assume A6: k <> 0 ; :: thesis:
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

let Y be set ; :: thesis:
let a be Element of Y; :: thesis:
set Y1 = the_subsets_of_card (n,(Y \ {a}));
assume A8: card Y = omega ; :: thesis:
then A9: Y is infinite ;
then reconsider Y1 = the_subsets_of_card (n,(Y \ {a})) as non empty set ;
deffunc H₁( Element of Y1) -> set = F . ($1 \/ {a});
assume A10: Y c= X ; :: thesis:
not Y is empty by A8;
then A11: {a} c= Y by ZFMISC_1:31;
A12: for x being Element of Y1 holds H₁(x) in k

proof

let x be Element of Y1; :: thesis:
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

assume a in x99 ; :: thesis:
then not a in {a} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

then card y = n + 1 by A13, A14, CARD_2:41;
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₁(x) in k by A6, A15, FUNCT_2:5; :: thesis:

end;

consider Fa being Function of Y1,k such that
A16: for x being Element of Y1 holds Fa . x = H₁(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:
take Ha ; :: thesis:
thus ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant ) by A18; :: thesis:
let Y9 be Element of the_subsets_of_card (n,(Y \ {a})); :: thesis:
thus Fa . Y9 = F . (Y9 \/ {a}) by A16; :: thesis:

end;

A19: for a being Nat
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₂[a,x99,y99,x199,y199]

proof

let a be Nat; :: thesis:
let x99 be Element of A; :: thesis:
let y99 be Element of omega ; :: thesis:

per cases ;

suppose A20: y99 in x99 ; :: thesis:

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:
take min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; :: thesis:
A26: Ha c= omega by A5, A25;

now :: thesis:

let x1, x2 be Element of A; :: thesis:
let y1, y2 be Element of omega ; :: thesis:
assume that
A27: x99 = x1 and
A28: y99 = y1 ; :: thesis:
assume that
A29: x199 = x2 and
A30: min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 ; :: thesis:
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:

proof

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:
take F1 ; :: thesis:
take H1 ; :: thesis:
for x being object st x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } holds
x in NAT

proof

let x be object ; :: thesis:
assume x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; :: thesis:
then ex x9 being Element of omega st
( x9 = x & x9 > y99 & x9 in Ha ) ;
hence x in NAT ; :: thesis:

end;

then reconsider A9 = { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } as Subset of NAT by TARSKI:def 3;
thus H1 is infinite by A22; :: thesis:
thus F1 | (the_subsets_of_card (n,H1)) is constant by A23; :: thesis:
thus x2 = H1 by A29; :: thesis:
A9 <> {}

proof

set A99 = { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ;

A31: now :: thesis:

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

per cases by A32, XBOOLE_0:def 3;

suppose x in A9 ; :: thesis:

then ex x9 being Element of omega st
( x = x9 & x9 > y99 & x9 in Ha ) ;
hence x in Ha ; :: thesis:

end;

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

then ex x9 being Element of omega st
( x = x9 & x9 <= y99 & x9 in Ha ) ;
hence x in Ha ; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; :: thesis:
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:

end;

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

A36: now :: thesis:

let x be object ; :: thesis:
assume A37: x in Ha ; :: thesis:
then reconsider x9 = x as Element of omega by A26;

per cases ;

suppose x9 <= y99 ; :: thesis:

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:

end;

suppose x9 > y99 ; :: thesis:

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

end;

assume A9 = {} ; :: thesis:
hence contradiction by A22, A35, A31, A36, TARSKI:2; :: thesis:

end;

then min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } in A9 by NAT_1:def 1;
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:
thus y1 < y2 by A28, A30, A38; :: thesis:
thus for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) by A24, A27, A28; :: thesis:
let y29 be Element of omega ; :: thesis:
assume A39: y29 > y1 ; :: thesis:
assume y29 in H1 ; :: thesis:
then y29 in A9 by A28, A39;
hence y2 <= y29 by A30, NAT_1:def 1; :: thesis:

end;

assume not y1 in x1 ; :: thesis:
hence S₂[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] by A20, A27, A28; :: thesis:

end;

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

end;

suppose A40: not y99 in x99 ; :: thesis:

reconsider y199 = 0 as Element of omega ;
reconsider x199 = X as Element of A by A4;
take x199 ; :: thesis:
take y199 ; :: thesis:
thus S₂[a,x99,y99,x199,y199] by A40; :: thesis:

end;

consider S being sequence of A, a being sequence of omega such that
A41: ( S . 0 = X0 & a . 0 = min* X & ( for i being Nat holds S₂[i,S . i,a . i,S . (i + 1),a . (i + 1)] ) ) from RECDEF_2:sch 3(A19);
defpred S₃[ 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₃[ 0 ]

proof

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:
thus S . (0 + 1) c= S . 0 by A3, A5, A41, A43, CARD_1:27, NAT_1:def 1, XBOOLE_1:1; :: thesis:
thus a . 0 in S . 0 by A3, A5, A41, CARD_1:27, NAT_1:def 1; :: thesis:
thus a . (0 + 1) in S . (0 + 1) by A3, A5, A41, A43, CARD_1:27, NAT_1:def 1; :: thesis:
not y1 in x2

proof

assume y1 in x2 ; :: thesis:
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:

end;

hence not a . 0 in S . (0 + 1) ; :: thesis:

end;

defpred S₄[ 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₅[ 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₃[i] holds
S₃[i + 1]

proof

let i be Nat; :: thesis:
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₃[i] ; :: thesis:
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

assume y1 in x2 ; :: thesis:
then not y1 in {y1} by A46, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

hence S₃[i + 1] by A45, A46, NAT_1:44, XBOOLE_1:1; :: thesis:

end;

A47: for i being Nat holds S₃[i] from NAT_1:sch 2(A42, A44);
A48: for l being Nat st S₅[l] holds
S₅[l + 1]

proof

let l be Nat; :: thesis:
assume A49: S₅[l] ; :: thesis:
thus S₅[l + 1] :: thesis:

proof

let i, j be Nat; :: thesis:
assume A50: i >= j ; :: thesis:
set j9 = j + 1;
assume A51: i = (l + 1) + j ; :: thesis:
then A52: i = l + (j + 1) ;
A53: S . (j + 1) c= S . j by A47;
i <> j

proof

assume i = j ; :: thesis:
then 0 = l + 1 by A51;
hence contradiction ; :: thesis:

end;

then i > j by A50, XXREAL_0:1;
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:
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:

proof

let ai, aj be Nat; :: thesis:
assume i <> j ; :: thesis:
assume that
A56: ai = a . i and
A57: aj = a . j ; :: thesis:
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:

end;

A58: S₅[ 0 ] ;
A59: for l being Nat holds S₅[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 ) )

proof

let i, j be Nat; :: thesis:
assume A61: i >= j ; :: thesis:
then A62: ex l being Nat st i = j + l by NAT_1:10;
hence S . i c= S . j by A59, A61; :: thesis:
thus for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds
ai > aj by A59, A61, A62; :: thesis:

end;

A63: for i being Element of NAT
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

let i be Element of NAT ; :: thesis:
let Y be set ; :: thesis:
let Fi be Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k; :: thesis:
assume A64: Y = { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > i ) } ; :: thesis:
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:
for x19 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds F1 . x19 = Fi . x19

proof

let x19 be Element of the_subsets_of_card (n,((S . i) \ {(a . i)})); :: thesis:
thus F1 . x19 = F . (x19 \/ {(a . i)}) by A67, A69
.= Fi . x19 by A70 ; :: thesis:

end;

then A71: Fi | (the_subsets_of_card (n,(S . (i + 1)))) is constant by A65, A68, FUNCT_2:63;

now :: thesis:

let x be object ; :: thesis:
assume x in Y ; :: thesis:
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 S . j c= S . (i + 1) by A60;
hence x in S . (i + 1) by A72, A47; :: thesis:

end;

hence Y c= S . (i + 1) ; :: thesis:
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

end;

hence Fi | (the_subsets_of_card (n,Y)) is constant by FUNCT_1:def 10; :: thesis:

end;

for x1, x2 being object st x1 in dom a & x2 in dom a & a . x1 = a . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis:
assume x1 in dom a ; :: thesis:
then reconsider i1 = x1 as Element of NAT ;
assume x2 in dom a ; :: thesis:
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:
assume A83: x1 <> x2 ; :: thesis:

per cases by A83, XXREAL_0:1;

suppose i1 < i2 ; :: thesis:

then ai1 < ai2 by A60;
hence contradiction by A82; :: thesis:

end;

suppose i1 > i2 ; :: thesis:

then ai1 > ai2 by A60;
hence contradiction by A82; :: thesis:

end;

then A84: a is one-to-one by FUNCT_1:def 4;
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

let i be Element of NAT ; :: thesis:
set Z = { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i ) } ;

now :: thesis:

let z be object ; :: thesis:
assume z in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i ) } ; :: thesis:
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:

end;

then A87: { x9 where x9 is Element of omega : ex j being Element of NAT st
( 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

let z be object ; :: thesis:

hereby :: thesis:

assume z in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i ) } ; :: thesis:
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:

end;

assume z in rng (a | (NAT \ (Segm (i + 1)))) ; :: thesis:
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 ;
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:

end;

then A94: { x9 where x9 is Element of omega : ex j being Element of NAT st
( 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:

end;

A95: for x being object st x in NAT holds
ex y being object st
( y in k & S₄[x,y] )

proof

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
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:

let x be object ; :: thesis:
assume x in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 ) } ; :: thesis:
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:

end;

then { x9 where x9 is Element of omega : ex j being Element of NAT st
( 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:
thus y in k by A6; :: thesis:
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

reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
let Y be set ; :: thesis:
let i be Element of NAT ; :: thesis:
let Fi be Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k; :: thesis:
assume A105: i = x ; :: thesis:
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:
assume A107: for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ; :: thesis:
take l ; :: thesis:
thus l = y ; :: thesis:
thus l in k by A6; :: thesis:
for x19 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fa . x19 = Fi . x19

proof

let x19 be Element of the_subsets_of_card (n,((S . i) \ {(a . i)})); :: thesis:
thus Fa . x19 = F . (x19 \/ {(a . i)}) by A98, A105
.= Fi . x19 by A107 ; :: thesis:

end;

hence rng (Fi | (the_subsets_of_card (n,Y))) = {l} by A104, A105, A106, FUNCT_2:63; :: thesis:

end;

hence S₄[x,y] ; :: thesis:

end;

consider g being sequence of k such that
A108: for x being object st x in NAT holds
S₄[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;

now :: thesis:

let y be object ; :: thesis:
assume y in a .: (g " {k9}) ; :: thesis:
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:

end;

then reconsider H = a .: (g " {k9}) as Subset of X by TARSKI:def 3;
take H = H; :: thesis:
thus H is infinite by A109, A110; :: thesis:
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

let y be set ; :: thesis:
assume y in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis:
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:

let x be object ; :: thesis:
assume A128: x in y \ {(min* Y)} ; :: thesis:
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

reconsider j = j as Element of NAT by A130;
take j ; :: thesis:
thus a . j = x9 by A131; :: thesis:
A133: min* Y <= x9 by A115, A117, A128, NAT_1:def 1;
thus j > x0 :: thesis:

proof

assume A134: x0 >= j ; :: thesis:
x0 <> j by A120, A132, A131, TARSKI:def 1;
hence contradiction by A60, A120, A131, A133, A134; :: thesis:

end;

hence x in { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 ) } ; :: thesis:

end;

then A135: y \ {(min* Y)} is Subset of { x where x is Element of omega : ex j being Element of NAT st
( 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:

end;

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
(F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y

proof

let x, y be object ; :: thesis:
assume x in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis:
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:
hence (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y by A113, A142; :: thesis:

end;

hence F | (the_subsets_of_card ((n + 1),H)) is constant by FUNCT_1:def 10; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

A143: S₁[ 0 ]

proof

let k be Nat; :: thesis:
let X be set ; :: thesis:
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:
assume A144: card X = omega ; :: thesis:
assume X c= omega ; :: thesis:
assume k <> 0 ; :: thesis:
take H ; :: thesis:
thus H is infinite by A144; :: thesis:
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

let x, y be object ; :: thesis:
assume A145: x in dom (F | (the_subsets_of_card (0,H))) ; :: thesis:
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:
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:

end;

hence F | (the_subsets_of_card (0,H)) is constant by FUNCT_1:def 10; :: thesis:

end;

for n being Nat holds S₁[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: