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]

proof

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

now

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 x1' being Element of the_subsets_of_card n,(x1 \ {y1}) holds F1 . x1' = F . (x1' \/ {y1}) ) & ( for y2' being Element of omega st y2' > y1 & y2' in H1 holds
y2 <= y2' ) ) ) & ( 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 Y' being Element of the_subsets_of_card n,(Y \ {a}) holds Fa . Y' = F . (Y' \/ {a}) ) )

proof

let Y be set ; :: thesis:
let a be Element of Y; :: thesis:
set Y1 = the_subsets_of_card n,(Y \ {a});
set Y' = 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 x' being Subset of (Y \ {a}) such that
A13: x = x' and
A14: card x' = 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 x'' = x' as finite set by A14;
not a in x''

proof

assume a in x'' ; :: 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 Y' be Element of the_subsets_of_card n,(Y \ {a}); :: thesis:
thus Fa . Y' = F . (Y' \/ {a}) by A16; :: thesis:

end;

A19: for a being Element of NAT
for x'' being Element of A
for y'' being Element of omega ex x1'' being Element of A ex y1'' being Element of omega st S₂[a,x'',y'',x1'',y1'']

proof

let a be Element of NAT ; :: thesis:
let x'' be Element of A; :: thesis:
let y'' be Element of omega ; :: thesis:

per cases ;

suppose A20: y'' in x'' ; :: thesis:

then reconsider a' = y'' as Element of x'' ;
A21: x'' in A ;
then ex x''' being Subset of X st
( x''' = x'' & card x''' = omega ) ;
then consider Fa being Function of (the_subsets_of_card n,(x'' \ {a'})),k, Ha being Subset of (x'' \ {a'}) such that
A22: not Ha is finite and
A23: Fa | (the_subsets_of_card n,Ha) is constant and
A24: for Y' being Element of the_subsets_of_card n,(x'' \ {a'}) holds Fa . Y' = F . (Y' \/ {a'}) by A7;
Ha c= x'' 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 x1'' = Ha as Element of A ;
set y1'' = min* { y2' where y2' is Element of omega : ( y2' > y'' & y2' in Ha ) } ;
take x1'' ; :: thesis:
take min* { y2' where y2' is Element of omega : ( y2' > y'' & y2' 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: x'' = x1 and
A28: y'' = y1 ; :: thesis:
assume that
A29: x1'' = x2 and
A30: min* { y2' where y2' is Element of omega : ( y2' > y'' & y2' 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 x1' being Element of the_subsets_of_card n,(x1 \ {y1}) holds F1 . x1' = F . (x1' \/ {y1}) ) & ( for y2' being Element of omega st y2' > y1 & y2' in H1 holds
y2 <= y2' ) ) ) :: thesis:

proof

reconsider H1 = Ha as Subset of (x1 \ {y1}) by A27, A28;
set A' = { y2' where y2' is Element of omega : ( y2' > y'' & y2' 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 { y2' where y2' is Element of omega : ( y2' > y'' & y2' in Ha ) } holds
x in NAT

proof

let x be set ; :: thesis:
assume x in { y2' where y2' is Element of omega : ( y2' > y'' & y2' in Ha ) } ; :: thesis:
then ex x' being Element of omega st
( x' = x & x' > y'' & x' in Ha ) ;
hence x in NAT ; :: thesis:

end;

then reconsider A' = { y2' where y2' is Element of omega : ( y2' > y'' & y2' 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:
A' <> {}

proof

set A'' = { y2''' where y2''' is Element of omega : ( y2''' <= y'' & y2''' in Ha ) } ;

A31: now

let x be set ; :: thesis:
assume A32: x in A' \/ { y2''' where y2''' is Element of omega : ( y2''' <= y'' & y2''' in Ha ) } ; :: thesis:

per cases by A32, XBOOLE_0:def 3;

suppose x in A' ; :: thesis:

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

end;

suppose x in { y2''' where y2''' is Element of omega : ( y2''' <= y'' & y2''' in Ha ) } ; :: thesis:

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

end;

now

let x be set ; :: thesis:
assume x in { y2''' where y2''' is Element of omega : ( y2''' <= y'' & y2''' in Ha ) } ; :: thesis:
then consider x' being Element of omega such that
A33: x = x' and
A34: x' <= y'' and
x' in Ha ;
x' < y'' + 1 by A34, NAT_1:13;
hence x in Segm (y'' + 1) by A33, NAT_1:45; :: thesis:

end;

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

A36: now

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

per cases ;

suppose x' <= y'' ; :: thesis:

then x in { y2''' where y2''' is Element of omega : ( y2''' <= y'' & y2''' in Ha ) } by A37;
hence x in A' \/ { y2''' where y2''' is Element of omega : ( y2''' <= y'' & y2''' in Ha ) } by XBOOLE_0:def 3; :: thesis:

end;

suppose x' > y'' ; :: thesis:

then x in A' by A37;
hence x in A' \/ { y2''' where y2''' is Element of omega : ( y2''' <= y'' & y2''' in Ha ) } by XBOOLE_0:def 3; :: thesis:

end;

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

end;

then min* { y2' where y2' is Element of omega : ( y2' > y'' & y2' in Ha ) } in A' by NAT_1:def 1;
then A38: ex y2'' being Element of omega st
( min* { y2' where y2' is Element of omega : ( y2' > y'' & y2' in Ha ) } = y2'' & y2'' > y'' & y2'' in Ha ) ;
hence y2 in H1 by A30; :: thesis:
thus y1 < y2 by A28, A30, A38; :: thesis:
thus for x1' being Element of the_subsets_of_card n,(x1 \ {y1}) holds F1 . x1' = F . (x1' \/ {y1}) by A24, A27, A28; :: thesis:
let y2' be Element of omega ; :: thesis:
assume A39: y2' > y1 ; :: thesis:
assume y2' in H1 ; :: thesis:
then y2' in A' by A28, A39;
hence y2 <= y2' by A30, NAT_1:def 1; :: thesis:

end;

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

end;

hence S₂[a,x'',y'',x1'', min* { y2' where y2' is Element of omega : ( y2' > y'' & y2' in Ha ) } ] ; :: thesis:

end;

suppose A40: not y'' in x'' ; :: thesis:

reconsider y1'' = 0 as Element of omega ;
reconsider x1'' = X as Element of A by A4;
take x1'' ; :: thesis:
take y1'' ; :: thesis:
thus S₂[a,x'',y'',x1'',y1''] 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 x1' being Element of the_subsets_of_card n,(x1 \ {y1}) holds F1 . x1' = F . (x1' \/ {y1}) ) & ( for y2' being Element of omega st y2' > y1 & y2' in H1 holds
y2 <= y2' ) ) ) 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 Y' being Element of the_subsets_of_card n,((S . i) \ {(a . i)}) holds Fi . Y' = F . (Y' \/ {(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 i' = i + 1 as Element of NAT by ORDINAL1:def 13;
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 ;
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 x1' being Element of the_subsets_of_card n,(x1 \ {y1}) holds F1 . x1' = F . (x1' \/ {y1}) ) & ( for y2' being Element of omega st y2' > y1 & y2' in H1 holds
y2 <= y2' ) ) 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 j' = 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, aj' being natural number st i <> j + 1 & ai = a . i & aj' = a . (j + 1) holds
ai > aj' 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:

per cases ;

suppose A58: i = j + 1 ; :: thesis:

a . j in a . (j + 1) by A47;
hence ai > aj by A56, A57, A58, NAT_1:45; :: thesis:

end;

suppose i <> j + 1 ; :: thesis:

reconsider aj' = a . (j + 1) as natural number ;
aj in aj' by A47, A57;
then aj' > 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 Y' being Element of the_subsets_of_card n,((S . i) \ {(a . i)}) holds Fi . Y' = F . (Y' \/ {(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 x1' being Element of the_subsets_of_card n,(x1 \ {y1}) holds F1 . x1' = F . (x1' \/ {y1}) ) & ( for y2' being Element of omega st y2' > y1 & y2' in H1 holds
y2 <= y2' ) ) & ( 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 x1' being Element of the_subsets_of_card n,(x1 \ {y1}) holds F1 . x1' = F . (x1' \/ {y1}) and
for y2' being Element of omega st y2' > y1 & y2' in H1 holds
y2 <= y2' by A47, A68;
reconsider F1 = F1 as Function of (the_subsets_of_card n,((S . i) \ {(a . i)})),k by A68;
assume A71: for Y' being Element of the_subsets_of_card n,((S . i) \ {(a . i)}) holds Fi . Y' = F . (Y' \/ {(a . i)}) ; :: thesis:
for x1' being Element of the_subsets_of_card n,((S . i) \ {(a . i)}) holds F1 . x1' = Fi . x1'

proof

let x1' be Element of the_subsets_of_card n,((S . i) \ {(a . i)}); :: thesis:
thus F1 . x1' = F . (x1' \/ {(a . i)}) by A68, A70
.= Fi . x1' 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 x' being Element of omega st
( x = x' & ex j being Element of NAT st
( a . j = x' & 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

let x, y be set ; :: thesis:
assume A77: x in dom (Fi | (the_subsets_of_card n,Y)) ; :: thesis:
then A78: x in the_subsets_of_card n,Y by RELAT_1:86;
x in dom Fi by A77, RELAT_1:86;
then A79: x in dom (Fi | (the_subsets_of_card n,(S . (i + 1)))) by A76, A78, RELAT_1:86;
assume A80: y in dom (Fi | (the_subsets_of_card n,Y)) ; :: thesis:
then A81: y in the_subsets_of_card n,Y by RELAT_1:86;
y in dom Fi by A80, RELAT_1:86;
then A82: y in dom (Fi | (the_subsets_of_card n,(S . (i + 1)))) by A76, A81, RELAT_1:86;
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 A76, FUNCT_1:82
.= (Fi | (the_subsets_of_card n,(S . (i + 1)))) . x by A78, FUNCT_1:72
.= (Fi | (the_subsets_of_card n,(S . (i + 1)))) . y by A72, A79, A82, FUNCT_1:def 16
.= ((Fi | (the_subsets_of_card n,(S . (i + 1)))) | (the_subsets_of_card n,Y)) . y by A81, FUNCT_1:72
.= (Fi | (the_subsets_of_card n,Y)) . y by A76, FUNCT_1:82 ; :: thesis:

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 { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i ) } = omega

proof

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

now

let z be set ; :: thesis:
assume z in { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i ) } ; :: thesis:
then ex z' being Element of omega st
( z = z' & ex j being Element of NAT st
( a . j = z' & j > i ) ) ;
hence z in NAT ; :: thesis:

end;

then A88: { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & 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 { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i ) } iff z in rng (a | (NAT \ (Segm (i + 1)))) )

proof

let z be set ; :: thesis:

hereby :: thesis:

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

end;

then A95: { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & 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 { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & 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 i' = x as Element of NAT ;
set Y' = S . i';
A97: not a . i' in S . (i' + 1) by A47;
reconsider a' = a . i' as Element of S . i' by A47;
set Z = { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } ;
A98: S . (i' + 1) c= S . i' by A47;
S . i' in A ;
then ex Y'' being Subset of X st
( Y'' = S . i' & card Y'' = omega ) ;
then consider Fa being Function of (the_subsets_of_card n,((S . i') \ {a'})),k, Ha being Subset of ((S . i') \ {a'}) such that
not Ha is finite and
Fa | (the_subsets_of_card n,Ha) is constant and
A99: for Y'' being Element of the_subsets_of_card n,((S . i') \ {a'}) holds Fa . Y'' = F . (Y'' \/ {a'}) by A7;
A100: { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } c= S . (i' + 1) by A64, A99;

now

let x be set ; :: thesis:
assume x in { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } ; :: thesis:
then A101: x in S . (i' + 1) by A100;
then not x in {(a . i')} by A97, TARSKI:def 1;
hence x in (S . i') \ {(a . i')} by A98, A101, XBOOLE_0:def 5; :: thesis:

end;

then { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } c= (S . i') \ {(a . i')} by TARSKI:def 3;
then the_subsets_of_card n,{ x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } c= the_subsets_of_card n,((S . i') \ {a'}) by Lm1;
then A102: Fa | (the_subsets_of_card n,{ x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } ) is Function of (the_subsets_of_card n,{ x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } ),k by A6, FUNCT_2:38;
A103: not card { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } c= card n by A87;
then not { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } is empty ;
then A104: not the_subsets_of_card n,{ x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } is empty by A103, GROUP_10:2;
Fa | (the_subsets_of_card n,{ x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } ) is constant by A64, A99;
then consider y being Element of k such that
A105: rng (Fa | (the_subsets_of_card n,{ x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } )) = {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 = { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i ) } & ( for Y' being Element of the_subsets_of_card n,((S . i) \ {(a . i)}) holds Fi . Y' = F . (Y' \/ {(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 k' = 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:
k' is Subset of NAT by STIRL2_1:8;
then reconsider l = y as natural number ;
assume A107: Y = { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i ) } ; :: thesis:
assume A108: for Y' being Element of the_subsets_of_card n,((S . i) \ {(a . i)}) holds Fi . Y' = F . (Y' \/ {(a . i)}) ; :: thesis:
take l ; :: thesis:
thus l = y ; :: thesis:
thus l in k by A6; :: thesis:
for x1' being Element of the_subsets_of_card n,((S . i) \ {(a . i)}) holds Fa . x1' = Fi . x1'

proof

let x1' be Element of the_subsets_of_card n,((S . i) \ {(a . i)}); :: thesis:
thus Fa . x1' = F . (x1' \/ {(a . i)}) by A99, A106
.= Fi . x1' 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 g' being Function st
( g = g' & dom g' = NAT & rng g' c= k ) by FUNCT_2:def 2;
then consider k' being set such that
k' in rng g and
A110: not g " {k'} is finite by COMPL_SP:24;
set H = a .: (g " {k'});
g " {k'} c= dom g by RELAT_1:167;
then g " {k'},a .: (g " {k'}) are_equipotent by A85, A86, CARD_1:60, XBOOLE_1:1;
then A111: card (g " {k'}) = card (a .: (g " {k'})) by CARD_1:21;

now

let y be set ; :: thesis:
assume y in a .: (g " {k'}) ; :: thesis:
then consider x being set such that
A112: [x,y] in a and
x in g " {k'} 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 " {k'}) 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 = k'

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 Y' = 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 " {k'} and
A121: min* Y = a . x0 by FUNCT_1:def 12;
consider y0' being set such that
y0' in rng g and
A122: [x0,y0'] in g and
A123: y0' in {k'} by A120, RELAT_1:166;
A124: x0 in dom g by A122, FUNCT_1:8;
A125: g . x0 = y0' 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 a' = 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) \ {a'})),k, H0 being Subset of ((S . x0) \ {a'}) such that
not H0 is finite and
F0 | (the_subsets_of_card n,H0) is constant and
A127: for Y' being Element of the_subsets_of_card n,((S . x0) \ {a'}) holds F0 . Y' = F . (Y' \/ {a'}) by A7;
reconsider y' = y as finite set by A116, A117;
card (y \ {(min* Y)}) c= card y' by CARD_1:27;
then reconsider Y'' = 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 " {k'} and
A132: x = a . j by A116, FUNCT_1:def 12;
reconsider x' = 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 = x' & j > x0 )

proof

reconsider j = j as Element of NAT by A131;
take j ; :: thesis:
thus a . j = x' by A132; :: thesis:
A134: min* Y <= x' 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 y' = (card Y'') + 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 ) } )) = {k'} 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 Y' = y \ {(min* Y)} as Element of the_subsets_of_card n,((S . x0) \ {(a . x0)}) by A140, A137;
Y' in dom F0 by A6, A141, FUNCT_2:def 1;
then Y' 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 ) } )) . Y' 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 ) } )) . Y' = k' by A138, TARSKI:def 1;
then A142: F0 . Y' = k' by A137, FUNCT_1:72;
F0 . Y' = F . (Y' \/ {(a . x0)}) by A127;
hence (F | (the_subsets_of_card (n + 1),H)) . y = k' 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 = k' 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: