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: S₁[ 0 ]

proof

let k be natural number ; :: thesis:
let X be set ; :: thesis:
let F be Function of (the_subsets_of_card 0 ,X),k; :: thesis:
assume A2: card X = omega ; :: thesis:
assume X c= omega ; :: thesis:
assume k <> 0 ; :: thesis:
set H = X;
A3: X c= X ;
reconsider H = X as Subset of X by A3;
take H ; :: thesis:
thus not H is finite by A2; :: 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:
A4: dom (F | (the_subsets_of_card 0 ,H)) = dom (F | {0 }) by Lm2
.= (dom F) /\ {0 } by RELAT_1:90 ;
assume x in dom (F | (the_subsets_of_card 0 ,H)) ; :: thesis:
then A5: x in {0 } by A4, XBOOLE_0:def 4;
assume y in dom (F | (the_subsets_of_card 0 ,H)) ; :: thesis:
then y in {0 } by A4, XBOOLE_0:def 4;
then y = 0 by TARSKI:def 1;
hence (F | (the_subsets_of_card 0 ,H)) . x = (F | (the_subsets_of_card 0 ,H)) . y by A5, TARSKI:def 1; :: thesis:

end;

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

end;

A6: for n being natural number st S₁[n] holds
S₁[n + 1]

proof

let n be natural number ; :: thesis:
assume A7: 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 A8: card X = omega ; :: thesis:
assume A9: X c= omega ; :: thesis:
assume A10: k <> 0 ; :: thesis:
A11: 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:
assume A12: card Y = omega ; :: thesis:
assume A13: Y c= X ; :: thesis:
set Y1 = the_subsets_of_card n,(Y \ {a});
A14: not Y is finite by A12;
not Y is empty by A12;
then A15: {a} c= Y by ZFMISC_1:37;
reconsider Y1 = the_subsets_of_card n,(Y \ {a}) as non empty set by A14;
deffunc H₁( Element of Y1) -> set = F . ($1 \/ {a});
A18: 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
A19: ( x = x' & card x' = n ) ;
x \/ {a} c= (Y \ {a}) \/ {a} by A19, XBOOLE_1:9;
then x \/ {a} c= Y \/ {a} by XBOOLE_1:39;
then reconsider y = x \/ {a} as Subset of Y by A15, XBOOLE_1:12;
reconsider x'' = x' as finite set by A19;
A20: 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;

A21: the_subsets_of_card (n + 1),Y c= the_subsets_of_card (n + 1),X by A13, Lm1;
card y = n + 1 by A19, A20, CARD_2:54;
then x \/ {a} in the_subsets_of_card (n + 1),Y ;
hence H₁(x) in k by A10, A21, FUNCT_2:7; :: thesis:

end;

consider Fa being Function of Y1,k such that
A22: for x being Element of Y1 holds Fa . x = H₁(x) from FUNCT_2:sch 8(A18);
reconsider Fa = Fa as Function of (the_subsets_of_card n,(Y \ {a})),k ;
set Y' = Y \ {a};
A23: Y c= omega by A9, A13, XBOOLE_1:1;
card (Y \ {a}) = omega by A14, A23, Th2, XBOOLE_1:1;
then consider Ha being Subset of (Y \ {a}) such that
A25: ( not Ha is finite & Fa | (the_subsets_of_card n,Ha) is constant ) by A7, A10, A23, XBOOLE_1:1;
take Fa ; :: thesis:
take Ha ; :: thesis:
thus ( not Ha is finite & Fa | (the_subsets_of_card n,Ha) is constant ) by A25; :: thesis:
let Y' be Element of the_subsets_of_card n,(Y \ {a}); :: thesis:
thus Fa . Y' = F . (Y' \/ {a}) by A22; :: thesis:

end;

X c= X ;
then A26: X in the_subsets_of_card omega ,X by A8;
then reconsider A = the_subsets_of_card omega ,X as non empty set ;
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 ) ) );
A27: 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 A28: y'' in x'' ; :: thesis:

then reconsider a' = y'' as Element of x'' ;
x'' in A ;
then consider x''' being Subset of X such that
A29: ( x''' = x'' & card x''' = omega ) ;
consider Fa being Function of (the_subsets_of_card n,(x'' \ {a'})),k, Ha being Subset of (x'' \ {a'}) such that
A30: ( not Ha is finite & Fa | (the_subsets_of_card n,Ha) is constant & ( for Y' being Element of the_subsets_of_card n,(x'' \ {a'}) holds Fa . Y' = F . (Y' \/ {a'}) ) ) by A11, A29;
Ha c= x'' by XBOOLE_1:1;
then A31: Ha c= X by A29, XBOOLE_1:1;
then A32: Ha c= omega by A9, XBOOLE_1:1;
card Ha = omega by A30, Th2, A9, A31, XBOOLE_1:1;
then Ha in A by A31;
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:

now

let x1, x2 be Element of A; :: thesis:
let y1, y2 be Element of omega ; :: thesis:
assume A33: ( x'' = x1 & y'' = y1 ) ; :: thesis:
assume A34: ( x1'' = x2 & 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

assume y1 in x1 ; :: thesis:
reconsider F1 = Fa as Function of (the_subsets_of_card n,(x1 \ {y1})),k by A33;
reconsider H1 = Ha as Subset of (x1 \ {y1}) by A33;
take F1 ; :: thesis:
take H1 ; :: thesis:
thus not H1 is finite by A30; :: thesis:
thus F1 | (the_subsets_of_card n,H1) is constant by A30; :: thesis:
thus x2 = H1 by A34; :: thesis:
set A' = { y2' where y2' is Element of omega : ( y2' > y'' & y2' in Ha ) } ;
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 consider x' being Element of omega such that
A35: ( x' = x & x' > y'' & x' in Ha ) ;
thus x in NAT by A35; :: 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;
A36: A' <> {}

proof

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

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
A38: ( x = x' & x' <= y'' & x' in Ha ) ;
x' < y'' + 1 by A38, NAT_1:13;
hence x in Segm (y'' + 1) by A38, NAT_1:45; :: thesis:

end;

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

A40: now

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

per cases by A41, XBOOLE_0:def 3;

suppose x in A' ; :: thesis:

then consider x' being Element of omega such that
A42: ( x = x' & x' > y'' & x' in Ha ) ;
thus x in Ha by A42; :: thesis:

end;

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

then consider x' being Element of omega such that
A43: ( x = x' & x' <= y'' & x' in Ha ) ;
thus x in Ha by A43; :: thesis:

end;

now

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

per cases ;

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

then x in { y2''' where y2''' is Element of omega : ( y2''' <= y'' & y2''' in Ha ) } by A44;
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 A44;
hence x in A' \/ { y2''' where y2''' is Element of omega : ( y2''' <= y'' & y2''' in Ha ) } by XBOOLE_0:def 3; :: thesis:

end;

hence contradiction by A30, A37, B39, A40, TARSKI:2; :: thesis:

end;

min* { y2' where y2' is Element of omega : ( y2' > y'' & y2' in Ha ) } in A' by A36, NAT_1:def 1;
then consider y2'' being Element of omega such that
A45: ( min* { y2' where y2' is Element of omega : ( y2' > y'' & y2' in Ha ) } = y2'' & y2'' > y'' & y2'' in Ha ) ;
thus y2 in H1 by A45, A34; :: thesis:
thus y1 < y2 by A45, A33, A34; :: thesis:
thus for x1' being Element of the_subsets_of_card n,(x1 \ {y1}) holds F1 . x1' = F . (x1' \/ {y1}) by A33, A30; :: thesis:
let y2' be Element of omega ; :: thesis:
assume A46: y2' > y1 ; :: thesis:
assume A47: y2' in H1 ; :: thesis:
y2' in A' by A46, A47, A33;
hence y2 <= y2' by A34, 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 A33, 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 A48: not y'' in x'' ; :: thesis:

reconsider x1'' = X as Element of A by A26;
reconsider y1'' = 0 as Element of omega by INT_1:16;
take x1'' ; :: thesis:
take y1'' ; :: thesis:
thus S₂[a,x'',y'',x1'',y1''] by A48; :: thesis:

end;

reconsider X0 = X as Element of A by A26;
set Y0 = min* X;
consider S being Function of NAT ,A, a being Function of NAT ,omega such that
A49: ( 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(A27);
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) );
A50: S₃[ 0 ]

proof

set i = 0 ;
reconsider i = 0 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 ;
S₂[i,S . i,a . i,S . (i + 1),a . (i + 1)] by A49;
then A51: ( ( 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 ) ) ) ;
consider F1 being Function of (the_subsets_of_card n,(x1 \ {y1})),k, H1 being Subset of (x1 \ {y1}) such that
A52: ( not H1 is finite & F1 | (the_subsets_of_card n,H1) is constant & x2 = H1 & y2 in H1 & y1 < y2 ) by A51, A49, A8, A9, CARD_1:47, NAT_1:def 1;
thus a . 0 in a . (0 + 1) by A52, NAT_1:45; :: thesis:
thus S . (0 + 1) c= S . 0 by A52, XBOOLE_1:1; :: thesis:
thus a . 0 in S . 0 by A49, A8, A9, CARD_1:47, NAT_1:def 1; :: thesis:
thus a . (0 + 1) in S . (0 + 1) by A52; :: thesis:
not y1 in x2

proof

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

end;

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

end;

A53: for i being natural number st S₃[i] holds
S₃[i + 1]

proof

let i be natural number ; :: thesis:
assume A54: S₃[i] ; :: 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 ;
consider F1 being Function of (the_subsets_of_card n,(x1 \ {y1})),k, H1 being Subset of (x1 \ {y1}) such that
A55: ( 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 A49, A54;
thus S₃[i + 1] :: thesis:

proof

thus a . (i + 1) in a . ((i + 1) + 1) by A55, NAT_1:45; :: thesis:
thus S . ((i + 1) + 1) c= S . (i + 1) by A55, XBOOLE_1:1; :: thesis:
thus a . (i + 1) in S . (i + 1) by A54; :: thesis:
thus a . ((i + 1) + 1) in S . ((i + 1) + 1) by A55; :: thesis:
not y1 in x2

proof

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

end;

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

end;

A56: for i being natural number holds S₃[i] from NAT_1:sch 2(A50, A53);
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 ) );
A57: S₄[ 0 ] ;
A58: for l being natural number st S₄[l] holds
S₄[l + 1]

proof

let l be natural number ; :: thesis:
assume A59: S₄[l] ; :: thesis:
thus S₄[l + 1] :: thesis:

proof

let i, j be natural number ; :: thesis:
assume A60: i >= j ; :: thesis:
assume A61: i = (l + 1) + j ; :: thesis:
i <> j

proof

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

end;

then A62: i > j by A60, XXREAL_0:1;
set j' = j + 1;
( i >= j + 1 & i = l + (j + 1) ) by A62, A61, NAT_1:13;
then A63: ( S . i c= S . (j + 1) & ( for ai, aj' being natural number st i <> j + 1 & ai = a . i & aj' = a . (j + 1) holds
ai > aj' ) ) by A59;
S . (j + 1) c= S . j by A56;
hence S . i c= S . j by A63, XBOOLE_1:1; :: thesis:
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 A64: ( ai = a . i & aj = a . j ) ; :: thesis:

per cases ;

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

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

end;

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

reconsider aj' = a . (j + 1) as natural number ;
aj in aj' by A64, A56;
then aj' > aj by NAT_1:45;
hence ai > aj by A63, A64, XXREAL_0:2; :: thesis:

end;

A66: for l being natural number holds S₄[l] from NAT_1:sch 2(A57, A58);
A67: 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 A68: i >= j ; :: thesis:
then consider l being natural number such that
A69: i = j + l by NAT_1:10;
thus S . i c= S . j by A66, A68, A69; :: thesis:
thus for ai, aj being natural number st i <> j & ai = a . i & aj = a . j holds
ai > aj by A66, A68, A69; :: thesis:

end;

A70: 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 A71: Y = { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > i ) } ; :: thesis:
assume A72: for Y' being Element of the_subsets_of_card n,((S . i) \ {(a . i)}) holds Fi . Y' = F . (Y' \/ {(a . i)}) ; :: thesis:
consider x1 being Element of A, y1 being Element of omega such that
A73: ( S . i = x1 & a . i = y1 ) ;
consider x2 being Element of A, y2 being Element of omega such that
A74: ( S . (i + 1) = x2 & a . (i + 1) = y2 ) ;
( 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 A49, A73, A74;
then consider F1 being Function of (the_subsets_of_card n,(x1 \ {y1})),k, H1 being Subset of (x1 \ {y1}) such that
A75: ( not H1 is finite & F1 | (the_subsets_of_card n,H1) is constant & x2 = H1 & ( 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 A73, A56;
reconsider F1 = F1 as Function of (the_subsets_of_card n,((S . i) \ {(a . i)})),k by A73;
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 A73, A75
.= Fi . x1' by A72 ; :: thesis:

end;

then A76: Fi | (the_subsets_of_card n,(S . (i + 1))) is constant by A75, A74, FUNCT_2:113;

now

let x be set ; :: thesis:
assume x in Y ; :: thesis:
then consider x' being Element of omega such that
A77: ( x = x' & ex j being Element of NAT st
( a . j = x' & j > i ) ) by A71;
consider j being Element of NAT such that
A78: ( a . j = x & j > i ) by A77;
j >= i + 1 by A78, NAT_1:13;
then A79: S . j c= S . (i + 1) by A67;
a . j in S . j by A56;
hence x in S . (i + 1) by A78, A79; :: thesis:

end;

hence A80: Y c= S . (i + 1) by TARSKI:def 3; :: thesis:
A81: the_subsets_of_card n,Y c= the_subsets_of_card n,(S . (i + 1)) by Lm1, A80;
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 x in dom (Fi | (the_subsets_of_card n,Y)) ; :: thesis:
then A82: ( x in dom Fi & x in the_subsets_of_card n,Y ) by RELAT_1:86;
then A83: x in dom (Fi | (the_subsets_of_card n,(S . (i + 1)))) by A81, RELAT_1:86;
assume y in dom (Fi | (the_subsets_of_card n,Y)) ; :: thesis:
then A84: ( y in dom Fi & y in the_subsets_of_card n,Y ) by RELAT_1:86;
then A85: y in dom (Fi | (the_subsets_of_card n,(S . (i + 1)))) by 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 A81, FUNCT_1:82
.= (Fi | (the_subsets_of_card n,(S . (i + 1)))) . x by A82, FUNCT_1:72
.= (Fi | (the_subsets_of_card n,(S . (i + 1)))) . y by A85, A76, A83, FUNCT_1:def 16
.= ((Fi | (the_subsets_of_card n,(S . (i + 1)))) | (the_subsets_of_card n,Y)) . y by A84, FUNCT_1:72
.= (Fi | (the_subsets_of_card n,Y)) . y by A81, 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 A86: x1 in dom a ; :: thesis:
assume A87: x2 in dom a ; :: thesis:
assume A88: a . x1 = a . x2 ; :: thesis:
assume A89: x1 <> x2 ; :: thesis:
reconsider i1 = x1 as Element of NAT by A86;
reconsider i2 = x2 as Element of NAT by A87;
reconsider ai1 = a . i1 as Element of NAT ;
reconsider ai2 = a . i2 as Element of NAT ;

per cases by A89, XXREAL_0:1;

suppose i1 < i2 ; :: thesis:

then ai1 < ai2 by A67;
hence contradiction by A88; :: thesis:

end;

suppose i1 > i2 ; :: thesis:

then ai1 > ai2 by A67;
hence contradiction by A88; :: thesis:

end;

then A90: a is one-to-one by FUNCT_1:def 8;
A91: NAT = dom a by FUNCT_2:def 1;
A92: 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 ) } ;
A93: 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 consider z' being Element of omega such that
A94: ( z = z' & ex j being Element of NAT st
( a . j = z' & j > i ) ) ;
consider j being Element of NAT such that
A95: ( a . j = z & j > i ) by A94;
j >= i + 1 by A95, NAT_1:13;
then not j in i + 1 by NAT_1:45;
then ( j in dom a & j in NAT \ (Segm (i + 1)) ) by A91, XBOOLE_0:def 5;
hence z in rng (a | (NAT \ (Segm (i + 1)))) by A95, FUNCT_1:73; :: thesis:

end;

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

end;

then A97: { 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;
A98: a | (NAT \ (Segm (i + 1))) is one-to-one by A90, FUNCT_1:84;

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 consider z' being Element of omega such that
A99: ( z = z' & ex j being Element of NAT st
( a . j = z' & j > i ) ) ;
thus z in NAT by A99; :: thesis:

end;

then { 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;
hence card { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i ) } = omega by A97, A93, Th2, A98, CARD_1:97; :: 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} );
A101: 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';
reconsider a' = a . i' as Element of S . i' by A56;
S . i' in A ;
then consider Y'' being Subset of X such that
A102: ( Y'' = S . i' & card Y'' = omega ) ;
consider Fa being Function of (the_subsets_of_card n,((S . i') \ {a'})),k, Ha being Subset of ((S . i') \ {a'}) such that
A103: ( not Ha is finite & Fa | (the_subsets_of_card n,Ha) is constant & ( for Y'' being Element of the_subsets_of_card n,((S . i') \ {a'}) holds Fa . Y'' = F . (Y'' \/ {a'}) ) ) by A102, A11;
set Z = { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } ;
A104: ( { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } c= S . (i' + 1) & 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 A70, A103;
A105: ( a . i' in a . (i' + 1) & S . (i' + 1) c= S . i' & a . i' in S . i' & a . (i' + 1) in S . (i' + 1) & not a . i' in S . (i' + 1) ) by A56;

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 A106: x in S . (i' + 1) by A104;
not x in {(a . i')} by A106, A105, TARSKI:def 1;
hence x in (S . i') \ {(a . i')} by A106, A105, 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 A107: 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;
A108: 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 A10, A107, FUNCT_2:38;
card { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } = omega by A92;
then not card { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } c= card n ;
then ( card n c= card { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } & not { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i' ) } is empty ) ;
then 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 GROUP_10:2;
then consider y being Element of k such that
A109: 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 A10, A108, A104, FUNCT_2:188;
reconsider y = y as set ;
take y ; :: thesis:
thus y in k by A10; :: thesis:
thus S₅[x,y] :: thesis:

proof

thus 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} ) :: thesis:

proof

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 A111: i = x ; :: thesis:
assume A112: Y = { x' where x' is Element of omega : ex j being Element of NAT st
( a . j = x' & j > i ) } ; :: thesis:
assume A113: for Y' being Element of the_subsets_of_card n,((S . i) \ {(a . i)}) holds Fi . Y' = F . (Y' \/ {(a . i)}) ; :: thesis:
reconsider k' = k as Element of NAT by ORDINAL1:def 13;
k' is Subset of NAT by STIRL2_1:8;
then reconsider l = y as natural number ;
take l ; :: thesis:
thus l = y ; :: thesis:
thus l in k by A10; :: 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 A111, A103
.= Fi . x1' by A113 ; :: thesis:

end;

hence rng (Fi | (the_subsets_of_card n,Y)) = {l} by A109, A112, A111, FUNCT_2:113; :: thesis:

end;

consider g being Function of NAT ,k such that
A114: for x being set st x in NAT holds
S₅[x,g . x] from FUNCT_2:sch 1(A101);
g in Funcs NAT ,k by A10, FUNCT_2:11;
then consider g' being Function such that
A116: ( g = g' & dom g' = NAT & rng g' c= k ) by FUNCT_2:def 2;
consider k' being set such that
A117: ( k' in rng g & not g " {k'} is finite ) by A116, COMPL_SP:24;
set H = a .: (g " {k'});
A118: g " {k'} c= dom g by RELAT_1:167;
g " {k'},a .: (g " {k'}) are_equipotent by A90, A91, A118, CARD_1:60, XBOOLE_1:1;
then A119: 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
A121: ( [x,y] in a & x in g " {k'} ) by RELAT_1:def 13;
A122: ( x in dom a & y = a . x ) by A121, FUNCT_1:8;
then reconsider i = x as Element of NAT ;
A123: y in S . i by A122, A56;
S . i in the_subsets_of_card omega ,X ;
then consider Xi being Subset of X such that
A124: ( S . i = Xi & card Xi = omega ) ;
thus y in X by A124, A123; :: 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 A117, A119; :: thesis:
A125: 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 A126: ( y in dom F & y in the_subsets_of_card (n + 1),H ) by RELAT_1:86;
then consider Y being Subset of H such that
A127: ( y = Y & card Y = n + 1 ) ;
set y0 = min* Y;
Y c= X by XBOOLE_1:1;
then A128: Y c= NAT by A9, XBOOLE_1:1;
then A129: ( min* Y in Y & ( for k being Element of NAT st k in Y holds
min* Y <= k ) ) by A127, CARD_1:47, NAT_1:def 1;
then consider x0 being set such that
A130: ( x0 in dom a & x0 in g " {k'} & min* Y = a . x0 ) by FUNCT_1:def 12;
consider y0' being set such that
A131: ( y0' in rng g & [x0,y0'] in g & y0' in {k'} ) by A130, RELAT_1:166;
A132: ( x0 in dom g & g . x0 = y0' ) by A131, FUNCT_1:8;
reconsider x0 = x0 as Element of NAT by A132;
reconsider a' = a . x0 as Element of S . x0 by A56;
S . x0 in the_subsets_of_card omega ,X ;
then consider S0 being Subset of X such that
A133: ( S0 = S . x0 & card S0 = omega ) ;
consider F0 being Function of (the_subsets_of_card n,((S . x0) \ {a'})),k, H0 being Subset of ((S . x0) \ {a'}) such that
A134: ( not H0 is finite & F0 | (the_subsets_of_card n,H0) is constant & ( for Y' being Element of the_subsets_of_card n,((S . x0) \ {a'}) holds F0 . Y' = F . (Y' \/ {a'}) ) ) by A11, A133;
set Y0 = { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 ) } ;
consider l being natural number such that
A135: ( 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 A114, A134;
A136: 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 A135, A132, A131, TARSKI:def 1;
set Y' = y \ {(min* Y)};
A137: ( { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 ) } c= S . (x0 + 1) & 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 ) } ) is constant ) by A70, A134;
A138: ( a . x0 in a . (x0 + 1) & S . (x0 + 1) c= S . x0 & a . x0 in S . x0 & a . (x0 + 1) in S . (x0 + 1) & not a . x0 in S . (x0 + 1) ) by A56;
A139: not a . x0 in { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 ) } by A137, A56;
{ x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 ) } c= S . x0 by A137, A138, XBOOLE_1:1;
then { 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;
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;

now

let x be set ; :: thesis:
assume A141: x in y \ {(min* Y)} ; :: thesis:
then A142: ( x in y & not x in {(min* Y)} ) by XBOOLE_0:def 5;
consider j being set such that
A143: ( j in dom a & j in g " {k'} & x = a . j ) by A142, A127, FUNCT_1:def 12;
reconsider x' = x as Element of omega by A142, A127, A128;
ex j being Element of NAT st
( a . j = x' & j > x0 )

proof

reconsider j = j as Element of NAT by A143;
take j ; :: thesis:
thus a . j = x' by A143; :: thesis:
A144: min* Y <= x' by A128, A141, A127, NAT_1:def 1;
thus j > x0 :: thesis:

proof

assume A145: x0 >= j ; :: thesis:
x0 <> j by A143, A142, A130, TARSKI:def 1;
hence contradiction by A144, A130, A145, A143, A67; :: 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 A146: 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;
A147: {(min* Y)} c= y by A127, A129, ZFMISC_1:37;
A148: (y \ {(min* Y)}) \/ {(a . x0)} = y by A130, A147, XBOOLE_1:45;
reconsider y' = y as finite set by A127;
card (y \ {(min* Y)}) c= card y' by CARD_1:27;
then reconsider Y'' = y \ {(min* Y)} as finite set ;
min* Y in {(min* Y)} by TARSKI:def 1;
then A149: not a . x0 in y \ {(min* Y)} by A130, XBOOLE_0:def 5;
card y' = (card Y'') + 1 by A148, A149, CARD_2:54;
then A150: 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 A127, A146;
then A151: y \ {(min* Y)} in the_subsets_of_card n,((S . x0) \ {(a . x0)}) by A140;
reconsider Y' = y \ {(min* Y)} as Element of the_subsets_of_card n,((S . x0) \ {(a . x0)}) by A140, A150;
Y' in dom F0 by A10, A151, 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 A150, 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 A136, TARSKI:def 1;
then A152: F0 . Y' = k' by A150, FUNCT_1:72;
F0 . Y' = F . (Y' \/ {(a . x0)}) by A134;
hence (F | (the_subsets_of_card (n + 1),H)) . y = k' by A152, A148, A126, 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 A153: (F | (the_subsets_of_card (n + 1),H)) . x = k' by A125;
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 A153, A125; :: 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;

for n being natural number holds S₁[n] from NAT_1:sch 2(A1, A6);
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: