let n, k be natural number ; :: thesis:
let X be set ; :: thesis:
defpred S₁[ natural number ] means for k being natural number
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
( not H is finite & F | (the_subsets_of_card $1,H) is constant );
A1: for n being natural number st S₁[n] holds
S₁[n + 1]

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

let k be natural number ; :: 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
( not H1 is finite & 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
( not Ha is finite & 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});
set Y9 = Y \ {a};
assume A8: card Y = omega ; :: thesis:
then A9: not Y is finite ;
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:37;
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:54;
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:7; :: 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, XBOOLE_1:1;
then card (Y \ {a}) = omega by A9, Th2, XBOOLE_1:1;
then consider Ha being Subset of (Y \ {a}) such that
A18: ( not Ha is finite & Fa | (the_subsets_of_card n,Ha) is constant ) by A2, A6, A17, XBOOLE_1:1;
take Fa ; :: thesis:
take Ha ; :: thesis:
thus ( not Ha is finite & 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 Element of 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 Element of 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: not Ha is finite 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, XBOOLE_1:1;

now

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
( not H1 is finite & 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 set st x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } holds
x in NAT

proof

let x be set ; :: 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 not H1 is finite 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

let x be set ; :: 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

let x be set ; :: 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:45; :: thesis:

end;

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

A36: now

let x be set ; :: 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 Function of NAT ,A, a being Function of NAT ,omega such that
A41: ( S . 0 = X0 & a . 0 = min* X & ( for i being Element of NAT holds S₂[i,S . i,a . i,S . (i + 1),a . (i + 1)] ) ) from RECDEF_2:sch 3(A19);
defpred S₃[ natural number ] means ( a . $1 in 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
( not H1 is finite & 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 a . (0 + 1) by A3, A5, A41, CARD_1:47, NAT_1:45, NAT_1:def 1; :: thesis:
thus S . (0 + 1) c= S . 0 by A3, A5, A41, A43, CARD_1:47, NAT_1:def 1, XBOOLE_1:1; :: thesis:
thus a . 0 in S . 0 by A3, A5, A41, CARD_1:47, NAT_1:def 1; :: thesis:
thus a . (0 + 1) in S . (0 + 1) by A3, A5, A41, A43, CARD_1:47, 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:47, 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₄[ set , set ] 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 natural number st
( l = $2 & l in k & rng (Fi | (the_subsets_of_card n,Y)) = {l} );
defpred S₅[ natural number ] means for i, j being natural number st i >= j & i = $1 + j holds
( S . i c= S . j & ( for ai, aj being natural number st i <> j & ai = a . i & aj = a . j holds
ai > aj ) );
A44: for i being natural number st S₃[i] holds
S₃[i + 1]

proof

let i be natural number ; :: 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
( not H1 is finite & 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:45, XBOOLE_1:1; :: thesis:

end;

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

proof

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

proof

let i, j be natural number ; :: 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, XBOOLE_1:1; :: thesis:
A55: for ai, aj9 being natural number st i <> j + 1 & ai = a . i & aj9 = a . (j + 1) holds
ai > aj9 by A49, A54, A52;
thus for ai, aj being natural number st i <> j & ai = a . i & aj = a . j holds
ai > aj :: thesis:

proof

let ai, aj be natural number ; :: thesis:
assume i <> j ; :: thesis:
assume that
A56: ai = a . i and
A57: aj = a . j ; :: thesis:
reconsider aj9 = a . (j + 1) as natural number ;
aj in aj9 by A47, A57;
then aj9 > aj by NAT_1:45;
hence ai > aj by A55, A56, XXREAL_0:2; :: thesis:

end;

A59: S₅[ 0 ] ;
A60: for l being natural number holds S₅[l] from NAT_1:sch 2(A59, A48);
A61: for i, j being natural number st i >= j holds
( S . i c= S . j & ( for ai, aj being natural number st i <> j & ai = a . i & aj = a . j holds
ai > aj ) )

proof

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

end;

A64: 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 A65: 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
A66: S . (i + 1) = x2 and
A67: a . (i + 1) = y2 ;
consider x1 being Element of A, y1 being Element of omega such that
A68: ( 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
( not H1 is finite & 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, A68, A66, A67;
then consider F1 being Function of (the_subsets_of_card n,(x1 \ {y1})),k, H1 being Subset of (x1 \ {y1}) such that
not H1 is finite and
A69: ( F1 | (the_subsets_of_card n,H1) is constant & x2 = H1 ) and
A70: 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, A68;
reconsider F1 = F1 as Function of (the_subsets_of_card n,((S . i) \ {(a . i)})),k by A68;
assume A71: 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 A68, A70
.= Fi . x19 by A71 ; :: thesis:

end;

then A72: Fi | (the_subsets_of_card n,(S . (i + 1))) is constant by A66, A69, FUNCT_2:113;

now

let x be set ; :: 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 A65;
then consider j being Element of NAT such that
A73: a . j = x and
A74: j > i ;
j >= i + 1 by A74, NAT_1:13;
then A75: S . j c= S . (i + 1) by A61;
a . j in S . j by A47;
hence x in S . (i + 1) by A73, A75; :: thesis:

end;

hence Y c= S . (i + 1) by TARSKI:def 3; :: thesis:
then A76: the_subsets_of_card n,Y c= the_subsets_of_card n,(S . (i + 1)) by Lm1;
for x, y being set 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 16; :: thesis:

end;

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

proof

let x1, x2 be set ; :: 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 A83: a . x1 = a . x2 ; :: thesis:
assume A84: x1 <> x2 ; :: thesis:

per cases by A84, XXREAL_0:1;

suppose i1 < i2 ; :: thesis:

then ai1 < ai2 by A61;
hence contradiction by A83; :: thesis:

end;

suppose i1 > i2 ; :: thesis:

then ai1 > ai2 by A61;
hence contradiction by A83; :: thesis:

end;

then A85: a is one-to-one by FUNCT_1:def 8;
A86: NAT = dom a by FUNCT_2:def 1;
A87: 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

let z be set ; :: 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 A88: { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i ) } c= NAT by TARSKI:def 3;
A89: dom (a | (NAT \ (Segm (i + 1)))) = (dom a) /\ (NAT \ (Segm (i + 1))) by RELAT_1:90
.= 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 set 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 set ; :: 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
A90: a . j = z and
A91: j > i ;
j >= i + 1 by A91, NAT_1:13;
then not j in i + 1 by NAT_1:45;
then j in NAT \ (Segm (i + 1)) by XBOOLE_0:def 5;
hence z in rng (a | (NAT \ (Segm (i + 1)))) by A86, A90, FUNCT_1:73; :: thesis:

end;

assume z in rng (a | (NAT \ (Segm (i + 1)))) ; :: thesis:
then consider j being set such that
A92: j in dom (a | (NAT \ (Segm (i + 1)))) and
A93: z = (a | (NAT \ (Segm (i + 1)))) . j by FUNCT_1:def 5;
reconsider j = j as Element of NAT by A92;
not j in Segm (i + 1) by A89, A92, XBOOLE_0:def 5;
then j >= i + 1 by NAT_1:45;
then A94: j > i by NAT_1:13;
a . j = z by A92, A93, FUNCT_1:70;
hence z in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i ) } by A94; :: thesis:

end;

then A95: { 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 A85, FUNCT_1:84;
hence card { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i ) } = omega by A89, A95, A88, Th2, CARD_1:97; :: thesis:

end;

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

proof

let x be set ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider i9 = x as Element of NAT ;
set Y9 = S . i9;
A97: 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 ) } ;
A98: 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
not Ha is finite and
Fa | (the_subsets_of_card n,Ha) is constant and
A99: for Y99 being Element of the_subsets_of_card n,((S . i9) \ {a9}) holds Fa . Y99 = F . (Y99 \/ {a9}) by A7;
A100: { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 ) } c= S . (i9 + 1) by A64, A99;

now

let x be set ; :: 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 A101: x in S . (i9 + 1) by A100;
then not x in {(a . i9)} by A97, TARSKI:def 1;
hence x in (S . i9) \ {(a . i9)} by A98, A101, 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)} by TARSKI:def 3;
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 A102: 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:38;
A103: 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 A87;
then not { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 ) } is empty ;
then A104: 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 A103, GROUP_10:2;
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 A64, A99;
then consider y being Element of k such that
A105: 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, A102, A104, FUNCT_2:188;
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 natural number 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 13;
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 A106: i = x ; :: thesis:
k9 is Subset of NAT by STIRL2_1:8;
then reconsider l = y as natural number ;
assume A107: Y = { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i ) } ; :: thesis:
assume A108: 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 A99, A106
.= Fi . x19 by A108 ; :: thesis:

end;

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

end;

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

end;

consider g being Function of NAT ,k such that
A109: for x being set st x in NAT holds
S₄[x,g . x] from FUNCT_2:sch 1(A96);
g in Funcs NAT ,k by A6, FUNCT_2:11;
then ex g9 being Function st
( g = g9 & dom g9 = NAT & rng g9 c= k ) by FUNCT_2:def 2;
then consider k9 being set such that
k9 in rng g and
A110: not g " {k9} is finite by COMPL_SP:24;
set H = a .: (g " {k9});
g " {k9} c= dom g by RELAT_1:167;
then g " {k9},a .: (g " {k9}) are_equipotent by A85, A86, CARD_1:60, XBOOLE_1:1;
then A111: card (g " {k9}) = card (a .: (g " {k9})) by CARD_1:21;

now

let y be set ; :: thesis:
assume y in a .: (g " {k9}) ; :: thesis:
then consider x being set such that
A112: [x,y] in a and
x in g " {k9} by RELAT_1:def 13;
x in dom a by A112, FUNCT_1:8;
then reconsider i = x as Element of NAT ;
y = a . x by A112, FUNCT_1:8;
then A113: y in S . i by A47;
S . i in the_subsets_of_card omega ,X ;
hence y in X by A113; :: thesis:

end;

then reconsider H = a .: (g " {k9}) as Subset of X by TARSKI:def 3;
take H = H; :: thesis:
thus not H is finite by A110, A111; :: thesis:
A114: 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 A115: y in the_subsets_of_card (n + 1),H by RELAT_1:86;
then consider Y being Subset of H such that
A116: y = Y and
A117: card Y = n + 1 ;
set y0 = min* Y;
set Y9 = y \ {(min* Y)};
Y c= X by XBOOLE_1:1;
then A118: Y c= NAT by A5, XBOOLE_1:1;
then A119: min* Y in Y by A117, CARD_1:47, NAT_1:def 1;
then consider x0 being set such that
x0 in dom a and
A120: x0 in g " {k9} and
A121: min* Y = a . x0 by FUNCT_1:def 12;
consider y09 being set such that
y09 in rng g and
A122: [x0,y09] in g and
A123: y09 in {k9} by A120, RELAT_1:166;
A124: x0 in dom g by A122, FUNCT_1:8;
A125: g . x0 = y09 by A122, FUNCT_1:8;
reconsider x0 = x0 as Element of NAT by A124;
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 A116, A119, ZFMISC_1:37;
then A126: (y \ {(min* Y)}) \/ {(a . x0)} = y by A121, 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
not H0 is finite and
F0 | (the_subsets_of_card n,H0) is constant and
A127: 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 A116, A117;
card (y \ {(min* Y)}) c= card y9 by CARD_1:27;
then reconsider Y99 = y \ {(min* Y)} as finite set ;
A128: { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 ) } c= S . (x0 + 1) by A64, A127;

now

let x be set ; :: thesis:
assume A129: x in y \ {(min* Y)} ; :: thesis:
then A130: x in y ;
then consider j being set such that
A131: j in dom a and
j in g " {k9} and
A132: x = a . j by A116, FUNCT_1:def 12;
reconsider x9 = x as Element of omega by A116, A118, A130;
A133: not x in {(min* Y)} by A129, 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 A131;
take j ; :: thesis:
thus a . j = x9 by A132; :: thesis:
A134: min* Y <= x9 by A116, A118, A129, NAT_1:def 1;
thus j > x0 :: thesis:

proof

assume A135: x0 >= j ; :: thesis:
x0 <> j by A121, A133, A132, TARSKI:def 1;
hence contradiction by A61, A121, A132, A134, A135; :: 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 A136: 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 A121, XBOOLE_0:def 5;
then card y9 = (card Y99) + 1 by A126, CARD_2:54;
then A137: 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 A116, A117, A136;
ex l being natural number 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 A109, A127;
then A138: 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 A123, A125, 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 A128, XBOOLE_1:1;
then A139: { 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, A128;
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 A139, ZFMISC_1:65;
then A140: 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 A141: y \ {(min* Y)} in the_subsets_of_card n,((S . x0) \ {(a . x0)}) by A137;
reconsider Y9 = y \ {(min* Y)} as Element of the_subsets_of_card n,((S . x0) \ {(a . x0)}) by A140, A137;
Y9 in dom F0 by A6, A141, 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 A137, RELAT_1:86;
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:12;
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 A138, TARSKI:def 1;
then A142: F0 . Y9 = k9 by A137, FUNCT_1:72;
F0 . Y9 = F . (Y9 \/ {(a . x0)}) by A127;
hence (F | (the_subsets_of_card (n + 1),H)) . y = k9 by A115, A126, A142, FUNCT_1:72; :: thesis:

end;

for x, y being set 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 set ; :: thesis:
assume x in dom (F | (the_subsets_of_card (n + 1),H)) ; :: thesis:
then A143: (F | (the_subsets_of_card (n + 1),H)) . x = k9 by A114;
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 A114, A143; :: thesis:

end;

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

end;

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

end;

A144: S₁[ 0 ]

proof

let k be natural number ; :: 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 A145: card X = omega ; :: thesis:
assume X c= omega ; :: thesis:
assume k <> 0 ; :: thesis:
take H ; :: thesis:
thus not H is finite by A145; :: thesis:
for x, y being set 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 set ; :: thesis:
assume A146: x in dom (F | (the_subsets_of_card 0 ,H)) ; :: thesis:
A147: dom (F | (the_subsets_of_card 0 ,H)) = dom (F | {0 }) by Lm2
.= (dom F) /\ {0 } by RELAT_1:90 ;
assume y in dom (F | (the_subsets_of_card 0 ,H)) ; :: thesis:
then y in {0 } by A147, XBOOLE_0:def 4;
then A148: y = 0 by TARSKI:def 1;
x in {0 } by A147, A146, XBOOLE_0:def 4;
hence (F | (the_subsets_of_card 0 ,H)) . x = (F | (the_subsets_of_card 0 ,H)) . y by A148, TARSKI:def 1; :: thesis:

end;

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

end;

for n being natural number holds S₁[n] from NAT_1:sch 2(A144, 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
( not H is finite & F | (the_subsets_of_card n,H) is constant ) ; :: thesis: