let n, k be Nat; :: thesis: for X being set
for F being Function of (the_subsets_of_card (n,X)),k st card X = omega & X c= omega & k <> 0 holds
ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

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

defpred S1[ Nat] means for k being Nat
for X being set
for F being Function of (the_subsets_of_card (\$1,X)),k st card X = omega & X c= omega & k <> 0 holds
ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card (\$1,H)) is constant );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
now :: thesis: for k being Nat
for X being set
for F being Function of (the_subsets_of_card ((n + 1),X)),k st card X = omega & X c= omega & k <> 0 holds
ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )
let k be Nat; :: thesis: for X being set
for F being Function of (the_subsets_of_card ((n + 1),X)),k st card X = omega & X c= omega & k <> 0 holds
ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

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

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

assume A3: card X = omega ; :: thesis: ( X c= omega & k <> 0 implies ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) )

X c= X ;
then A4: X in the_subsets_of_card (omega,X) by A3;
then reconsider A = the_subsets_of_card (omega,X) as non empty set ;
reconsider X0 = X as Element of A by A4;
defpred S2[ set , set , set , set , set ] means for x1, x2 being Element of A
for y1, y2 being Element of omega st \$2 = x1 & \$3 = y1 & \$4 = x2 & \$5 = y2 holds
( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) ) ) & ( not y1 in x1 implies ( x2 = X & y2 = 0 ) ) );
set Y0 = min* X;
assume A5: X c= omega ; :: thesis: ( k <> 0 implies ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant ) )

assume A6: k <> 0 ; :: thesis: ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )

A7: for Y being set
for a being Element of Y st card Y = omega & Y c= X holds
ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st
( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )
proof
let Y be set ; :: thesis: for a being Element of Y st card Y = omega & Y c= X holds
ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st
( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

let a be Element of Y; :: thesis: ( card Y = omega & Y c= X implies ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st
( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) )

set Y1 = the_subsets_of_card (n,(Y \ {a}));
assume A8: card Y = omega ; :: thesis: ( not Y c= X or ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st
( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) ) )

then A9: Y is infinite ;
then reconsider Y1 = the_subsets_of_card (n,(Y \ {a})) as non empty set ;
deffunc H1( Element of Y1) -> set = F . (\$1 \/ {a});
assume A10: Y c= X ; :: thesis: ex Fa being Function of (the_subsets_of_card (n,(Y \ {a}))),k ex Ha being Subset of (Y \ {a}) st
( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

not Y is empty by A8;
then A11: {a} c= Y by ZFMISC_1:31;
A12: for x being Element of Y1 holds H1(x) in k
proof
let x be Element of Y1; :: thesis: H1(x) in k
x in Y1 ;
then consider x9 being Subset of (Y \ {a}) such that
A13: x = x9 and
A14: card x9 = n ;
x \/ {a} c= (Y \ {a}) \/ {a} by ;
then x \/ {a} c= Y \/ {a} by XBOOLE_1:39;
then reconsider y = x \/ {a} as Subset of Y by ;
reconsider x99 = x9 as finite set by A14;
not a in x99 then card y = n + 1 by ;
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 ;
hence H1(x) in k by ; :: thesis: verum
end;
consider Fa being Function of Y1,k such that
A16: for x being Element of Y1 holds Fa . x = H1(x) from reconsider Fa = Fa as Function of (the_subsets_of_card (n,(Y \ {a}))),k ;
A17: Y c= omega by ;
then card (Y \ {a}) = omega by ;
then consider Ha being Subset of (Y \ {a}) such that
A18: ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant ) by ;
take Fa ; :: thesis: ex Ha being Subset of (Y \ {a}) st
( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )

take Ha ; :: thesis: ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant & ( for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a}) ) )
thus ( Ha is infinite & Fa | (the_subsets_of_card (n,Ha)) is constant ) by A18; :: thesis: for Y9 being Element of the_subsets_of_card (n,(Y \ {a})) holds Fa . Y9 = F . (Y9 \/ {a})
let Y9 be Element of the_subsets_of_card (n,(Y \ {a})); :: thesis: Fa . Y9 = F . (Y9 \/ {a})
thus Fa . Y9 = F . (Y9 \/ {a}) by A16; :: thesis: verum
end;
A19: for a being Nat
for x99 being Element of A
for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199]
proof
let a be Nat; :: thesis: for x99 being Element of A
for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199]

let x99 be Element of A; :: thesis: for y99 being Element of omega ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199]
let y99 be Element of omega ; :: thesis: ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199]
per cases ( y99 in x99 or not y99 in x99 ) ;
suppose A20: y99 in x99 ; :: thesis: ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199]
then reconsider a9 = y99 as Element of x99 ;
A21: x99 in A ;
then ex x999 being Subset of X st
( x999 = x99 & card x999 = omega ) ;
then consider Fa being Function of (the_subsets_of_card (n,(x99 \ {a9}))),k, Ha being Subset of (x99 \ {a9}) such that
A22: Ha is infinite and
A23: Fa | (the_subsets_of_card (n,Ha)) is constant and
A24: for Y9 being Element of the_subsets_of_card (n,(x99 \ {a9})) holds Fa . Y9 = F . (Y9 \/ {a9}) by A7;
Ha c= x99 by XBOOLE_1:1;
then A25: Ha c= X by ;
then card Ha = omega by ;
then Ha in A by A25;
then reconsider x199 = Ha as Element of A ;
set y199 = min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ;
take x199 ; :: thesis: ex y199 being Element of omega st S2[a,x99,y99,x199,y199]
take min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; :: thesis: S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ]
A26: Ha c= omega by ;
now :: thesis: for x1, x2 being Element of A
for y1, y2 being Element of omega st x99 = x1 & y99 = y1 & x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 holds
( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) ) ) & ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) )
let x1, x2 be Element of A; :: thesis: for y1, y2 being Element of omega st x99 = x1 & y99 = y1 & x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 holds
( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) ) ) & ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) )

let y1, y2 be Element of omega ; :: thesis: ( x99 = x1 & y99 = y1 & x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 implies ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) ) ) & ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) ) )

assume that
A27: x99 = x1 and
A28: y99 = y1 ; :: thesis: ( x199 = x2 & min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 implies ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) ) ) & ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) ) )

assume that
A29: x199 = x2 and
A30: min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } = y2 ; :: thesis: ( ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) ) ) & ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ) )

thus ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) ) ) :: thesis: ( not y1 in x1 implies S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] )
proof
reconsider H1 = Ha as Subset of (x1 \ {y1}) by ;
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 ;
assume y1 in x1 ; :: thesis: ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) )

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

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

for x being object st x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } holds
x in NAT
proof
let x be object ; :: thesis: ( x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } implies x in NAT )
assume x in { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ; :: thesis:
then ex x9 being Element of omega st
( x9 = x & x9 > y99 & x9 in Ha ) ;
hence x in NAT ; :: thesis: verum
end;
then reconsider A9 = { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } as Subset of NAT by TARSKI:def 3;
thus H1 is infinite by A22; :: thesis: ( F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) )

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

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

A9 <> {}
proof
set A99 = { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ;
A31: now :: thesis: for x being object st x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } holds
x in Ha
let x be object ; :: thesis: ( x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } implies b1 in Ha )
assume A32: x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; :: thesis: b1 in Ha
per cases ( x in A9 or x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ) by ;
suppose x in A9 ; :: thesis: b1 in Ha
then ex x9 being Element of omega st
( x = x9 & x9 > y99 & x9 in Ha ) ;
hence x in Ha ; :: thesis: verum
end;
suppose x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; :: thesis: b1 in Ha
then ex x9 being Element of omega st
( x = x9 & x9 <= y99 & x9 in Ha ) ;
hence x in Ha ; :: thesis: verum
end;
end;
end;
now :: thesis: for x being object st x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } holds
x in Segm (y99 + 1)
let x be object ; :: thesis: ( x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } implies x in Segm (y99 + 1) )
assume x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } ; :: thesis: x in Segm (y99 + 1)
then consider x9 being Element of omega such that
A33: x = x9 and
A34: x9 <= y99 and
x9 in Ha ;
x9 < y99 + 1 by ;
hence x in Segm (y99 + 1) by ; :: thesis: verum
end;
then A35: { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } c= Segm (y99 + 1) ;
A36: now :: thesis: for x being object st x in Ha holds
x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) }
let x be object ; :: thesis: ( x in Ha implies b1 in A9 \/ { b2 where y2999 is Element of omega : ( b2 <= y99 & b2 in Ha ) } )
assume A37: x in Ha ; :: thesis: b1 in A9 \/ { b2 where y2999 is Element of omega : ( b2 <= y99 & b2 in Ha ) }
then reconsider x9 = x as Element of omega by A26;
per cases ( x9 <= y99 or x9 > y99 ) ;
suppose x9 <= y99 ; :: thesis: b1 in A9 \/ { b2 where y2999 is Element of omega : ( b2 <= y99 & b2 in Ha ) }
then x in { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } by A37;
hence x in A9 \/ { y2999 where y2999 is Element of omega : ( y2999 <= y99 & y2999 in Ha ) } by XBOOLE_0:def 3; :: thesis: verum
end;
suppose x9 > y99 ; :: thesis: b1 in A9 \/ { b2 where y2999 is Element of omega : ( b2 <= y99 & b2 in Ha ) }
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: verum
end;
end;
end;
assume A9 = {} ; :: thesis: contradiction
hence contradiction by A22, A35, A31, A36, TARSKI:2; :: thesis: verum
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: ( y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) )

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

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

let y29 be Element of omega ; :: thesis: ( y29 > y1 & y29 in H1 implies y2 <= y29 )
assume A39: y29 > y1 ; :: thesis: ( not y29 in H1 or y2 <= y29 )
assume y29 in H1 ; :: thesis: y2 <= y29
then y29 in A9 by ;
hence y2 <= y29 by ; :: thesis: verum
end;
assume not y1 in x1 ; :: thesis: S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ]
hence S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] by ; :: thesis: verum
end;
hence S2[a,x99,y99,x199, min* { y29 where y29 is Element of omega : ( y29 > y99 & y29 in Ha ) } ] ; :: thesis: verum
end;
suppose A40: not y99 in x99 ; :: thesis: ex x199 being Element of A ex y199 being Element of omega st S2[a,x99,y99,x199,y199]
reconsider y199 = 0 as Element of omega ;
reconsider x199 = X as Element of A by A4;
take x199 ; :: thesis: ex y199 being Element of omega st S2[a,x99,y99,x199,y199]
take y199 ; :: thesis: S2[a,x99,y99,x199,y199]
thus S2[a,x99,y99,x199,y199] by A40; :: thesis: verum
end;
end;
end;
consider S being sequence of A, a being sequence of omega such that
A41: ( S . 0 = X0 & a . 0 = min* X & ( for i being Nat holds S2[i,S . i,a . i,S . (i + 1),a . (i + 1)] ) ) from defpred S3[ Nat] means ( a . \$1 in Segm (a . (\$1 + 1)) & S . (\$1 + 1) c= S . \$1 & a . \$1 in S . \$1 & a . (\$1 + 1) in S . (\$1 + 1) & not a . \$1 in S . (\$1 + 1) );
A42: S3[ 0 ]
proof
set i = 0 ;
reconsider i = 0 as Element of NAT ;
reconsider x1 = S . i as Element of A ;
reconsider x2 = S . (i + 1) as Element of A ;
reconsider y1 = a . i as Element of omega ;
reconsider y2 = a . (i + 1) as Element of omega ;
A43: ( y1 in x1 implies ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) ) ) by A41;
hence a . 0 in Segm (a . (0 + 1)) by ; :: thesis: ( S . (0 + 1) c= S . 0 & a . 0 in S . 0 & a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) )
thus S . (0 + 1) c= S . 0 by ; :: thesis: ( a . 0 in S . 0 & a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) )
thus a . 0 in S . 0 by ; :: thesis: ( a . (0 + 1) in S . (0 + 1) & not a . 0 in S . (0 + 1) )
thus a . (0 + 1) in S . (0 + 1) by ; :: thesis: not a . 0 in S . (0 + 1)
not y1 in x2 hence not a . 0 in S . (0 + 1) ; :: thesis: verum
end;
defpred S4[ object , object ] means for Y being set
for i being Element of NAT
for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = \$1 & Y = { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > i )
}
& ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds
ex l being Nat st
( l = \$2 & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} );
defpred S5[ Nat] means for i, j being Nat st i >= j & i = \$1 + j holds
( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds
ai > aj ) );
A44: for i being Nat st S3[i] holds
S3[i + 1]
proof
let i be Nat; :: thesis: ( S3[i] implies S3[i + 1] )
reconsider i9 = i + 1 as Element of NAT ;
reconsider x1 = S . i9 as Element of A ;
reconsider x2 = S . (i9 + 1) as Element of A ;
reconsider y1 = a . i9 as Element of omega ;
reconsider y2 = a . (i9 + 1) as Element of omega ;
assume A45: S3[i] ; :: thesis: S3[i + 1]
then A46: ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) ) by A41;
not y1 in x2 hence S3[i + 1] by ; :: thesis: verum
end;
A47: for i being Nat holds S3[i] from A48: for l being Nat st S5[l] holds
S5[l + 1]
proof
let l be Nat; :: thesis: ( S5[l] implies S5[l + 1] )
assume A49: S5[l] ; :: thesis: S5[l + 1]
thus S5[l + 1] :: thesis: verum
proof
let i, j be Nat; :: thesis: ( i >= j & i = (l + 1) + j implies ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds
ai > aj ) ) )

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

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

then A52: i = l + (j + 1) ;
A53: S . (j + 1) c= S . j by A47;
i <> j
proof
assume i = j ; :: thesis: contradiction
then 0 = l + 1 by A51;
hence contradiction ; :: thesis: verum
end;
then i > j by ;
then A54: i >= j + 1 by NAT_1:13;
then S . i c= S . (j + 1) by ;
hence S . i c= S . j by A53; :: thesis: for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds
ai > aj

A55: for ai, aj9 being Nat st i <> j + 1 & ai = a . i & aj9 = a . (j + 1) holds
ai > aj9 by ;
thus for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds
ai > aj :: thesis: verum
proof
let ai, aj be Nat; :: thesis: ( i <> j & ai = a . i & aj = a . j implies ai > aj )
assume i <> j ; :: thesis: ( not ai = a . i or not aj = a . j or ai > aj )
assume that
A56: ai = a . i and
A57: aj = a . j ; :: thesis: ai > aj
reconsider aj9 = a . (j + 1) as Nat ;
aj in Segm aj9 by ;
then aj9 > aj by NAT_1:44;
hence ai > aj by ; :: thesis: verum
end;
end;
end;
A58: S5[ 0 ] ;
A59: for l being Nat holds S5[l] from A60: for i, j being Nat st i >= j holds
( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds
ai > aj ) )
proof
let i, j be Nat; :: thesis: ( i >= j implies ( S . i c= S . j & ( for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds
ai > aj ) ) )

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

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

thus for ai, aj being Nat st i <> j & ai = a . i & aj = a . j holds
ai > aj by ; :: thesis: verum
end;
A63: for i being Element of NAT
for Y being set
for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st Y = { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > i )
}
& ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds
( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )
proof
let i be Element of NAT ; :: thesis: for Y being set
for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st Y = { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > i )
}
& ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds
( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )

let Y be set ; :: thesis: for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st Y = { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > i )
}
& ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds
( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )

let Fi be Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k; :: thesis: ( Y = { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > i )
}
& ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) implies ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) )

assume A64: Y = { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > i )
}
; :: thesis: ( ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant ) )
consider x2 being Element of A, y2 being Element of omega such that
A65: S . (i + 1) = x2 and
A66: a . (i + 1) = y2 ;
consider x1 being Element of A, y1 being Element of omega such that
A67: ( S . i = x1 & a . i = y1 ) ;
( y1 in x1 implies ( ex F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k ex H1 being Subset of (x1 \ {y1}) st
( H1 is infinite & F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 & y2 in H1 & y1 < y2 & ( for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) ) & ( for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 ) ) & ( not y1 in x1 implies ( x2 = X & y2 = 0 ) ) ) ) by A41, A67, A65, A66;
then consider F1 being Function of (the_subsets_of_card (n,(x1 \ {y1}))),k, H1 being Subset of (x1 \ {y1}) such that
H1 is infinite and
A68: ( F1 | (the_subsets_of_card (n,H1)) is constant & x2 = H1 ) and
A69: for x19 being Element of the_subsets_of_card (n,(x1 \ {y1})) holds F1 . x19 = F . (x19 \/ {y1}) and
for y29 being Element of omega st y29 > y1 & y29 in H1 holds
y2 <= y29 by ;
reconsider F1 = F1 as Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k by A67;
assume A70: for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ; :: thesis: ( Y c= S . (i + 1) & Fi | (the_subsets_of_card (n,Y)) is constant )
for x19 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds F1 . x19 = Fi . x19
proof
let x19 be Element of the_subsets_of_card (n,((S . i) \ {(a . i)})); :: thesis: F1 . x19 = Fi . x19
thus F1 . x19 = F . (x19 \/ {(a . i)}) by
.= Fi . x19 by A70 ; :: thesis: verum
end;
then A71: Fi | (the_subsets_of_card (n,(S . (i + 1)))) is constant by ;
now :: thesis: for x being object st x in Y holds
x in S . (i + 1)
let x be object ; :: thesis: ( x in Y implies x in S . (i + 1) )
assume x in Y ; :: thesis: x in S . (i + 1)
then ex x9 being Element of omega st
( x = x9 & ex j being Element of NAT st
( a . j = x9 & j > i ) ) by A64;
then consider j being Element of NAT such that
A72: a . j = x and
A73: j > i ;
j >= i + 1 by ;
then A74: S . j c= S . (i + 1) by A60;
a . j in S . j by A47;
hence x in S . (i + 1) by ; :: thesis: verum
end;
hence Y c= S . (i + 1) ; :: thesis: Fi | (the_subsets_of_card (n,Y)) is constant
then A75: the_subsets_of_card (n,Y) c= the_subsets_of_card (n,(S . (i + 1))) by Lm1;
for x, y being object st x in dom (Fi | (the_subsets_of_card (n,Y))) & y in dom (Fi | (the_subsets_of_card (n,Y))) holds
(Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y
proof
let x, y be object ; :: thesis: ( x in dom (Fi | (the_subsets_of_card (n,Y))) & y in dom (Fi | (the_subsets_of_card (n,Y))) implies (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y )
assume A76: x in dom (Fi | (the_subsets_of_card (n,Y))) ; :: thesis: ( not y in dom (Fi | (the_subsets_of_card (n,Y))) or (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y )
then A77: x in the_subsets_of_card (n,Y) ;
x in dom Fi by ;
then A78: x in dom (Fi | (the_subsets_of_card (n,(S . (i + 1))))) by ;
assume A79: y in dom (Fi | (the_subsets_of_card (n,Y))) ; :: thesis: (Fi | (the_subsets_of_card (n,Y))) . x = (Fi | (the_subsets_of_card (n,Y))) . y
then A80: y in the_subsets_of_card (n,Y) ;
y in dom Fi by ;
then A81: y in dom (Fi | (the_subsets_of_card (n,(S . (i + 1))))) by ;
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
.= (Fi | (the_subsets_of_card (n,(S . (i + 1))))) . x by
.= (Fi | (the_subsets_of_card (n,(S . (i + 1))))) . y by
.= ((Fi | (the_subsets_of_card (n,(S . (i + 1))))) | (the_subsets_of_card (n,Y))) . y by
.= (Fi | (the_subsets_of_card (n,Y))) . y by ; :: thesis: verum
end;
hence Fi | (the_subsets_of_card (n,Y)) is constant by FUNCT_1:def 10; :: thesis: verum
end;
for x1, x2 being object st x1 in dom a & x2 in dom a & a . x1 = a . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom a & x2 in dom a & a . x1 = a . x2 implies x1 = x2 )
assume x1 in dom a ; :: thesis: ( not x2 in dom a or not a . x1 = a . x2 or x1 = x2 )
then reconsider i1 = x1 as Element of NAT ;
assume x2 in dom a ; :: thesis: ( not a . x1 = a . x2 or x1 = x2 )
then reconsider i2 = x2 as Element of NAT ;
reconsider ai2 = a . i2 as Element of NAT ;
reconsider ai1 = a . i1 as Element of NAT ;
assume A82: a . x1 = a . x2 ; :: thesis: x1 = x2
assume A83: x1 <> x2 ; :: thesis: contradiction
per cases ( i1 < i2 or i1 > i2 ) by ;
end;
end;
then A84: a is one-to-one by FUNCT_1:def 4;
A85: NAT = dom a by FUNCT_2:def 1;
A86: for i being Element of NAT holds card { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
= omega
proof
let i be Element of NAT ; :: thesis: card { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
= omega

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

assume z in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
; :: thesis:
then ex z9 being Element of omega st
( z = z9 & ex j being Element of NAT st
( a . j = z9 & j > i ) ) ;
hence z in NAT ; :: thesis: verum
end;
then A87: { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i ) } c= NAT ;
A88: dom (a | (NAT \ (Segm (i + 1)))) = (dom a) /\ (NAT \ (Segm (i + 1))) by RELAT_1:61
.= NAT /\ (NAT \ (Segm (i + 1))) by FUNCT_2:def 1
.= () \ (Segm (i + 1)) by XBOOLE_1:49
.= NAT \ (Segm (i + 1)) ;
for z being object holds
( z in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
iff z in rng (a | (NAT \ (Segm (i + 1)))) )
proof
let z be object ; :: thesis: ( 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)))) )

hereby :: thesis: ( z in rng (a | (NAT \ (Segm (i + 1)))) implies z in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
)
assume z in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
; :: thesis: z in rng (a | (NAT \ (Segm (i + 1))))
then ex z9 being Element of omega st
( z = z9 & ex j being Element of NAT st
( a . j = z9 & j > i ) ) ;
then consider j being Element of NAT such that
A89: a . j = z and
A90: j > i ;
j >= i + 1 by ;
then not j in Segm (i + 1) by NAT_1:44;
then j in NAT \ (Segm (i + 1)) by XBOOLE_0:def 5;
hence z in rng (a | (NAT \ (Segm (i + 1)))) by ; :: thesis: verum
end;
assume z in rng (a | (NAT \ (Segm (i + 1)))) ; :: thesis: z in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}

then consider j being object such that
A91: j in dom (a | (NAT \ (Segm (i + 1)))) and
A92: z = (a | (NAT \ (Segm (i + 1)))) . j by FUNCT_1:def 3;
j in dom a by ;
then reconsider j = j as Element of NAT ;
dom (a | (NAT \ (Segm (i + 1)))) c= NAT \ (Segm (i + 1)) by RELAT_1:58;
then not j in Segm (i + 1) by ;
then j >= i + 1 by NAT_1:44;
then A93: j > i by NAT_1:13;
a . j = z by ;
hence z in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
by A93; :: thesis: verum
end;
then A94: { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i ) } = rng (a | (NAT \ (Segm (i + 1)))) by TARSKI:2;
a | (NAT \ (Segm (i + 1))) is one-to-one by ;
hence card { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
= omega by ; :: thesis: verum
end;
A95: for x being object st x in NAT holds
ex y being object st
( y in k & S4[x,y] )
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in k & S4[x,y] ) )

assume x in NAT ; :: thesis: ex y being object st
( y in k & S4[x,y] )

then reconsider i9 = x as Element of NAT ;
set Y9 = S . i9;
A96: not a . i9 in S . (i9 + 1) by A47;
reconsider a9 = a . i9 as Element of S . i9 by A47;
set Z = { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 )
}
;
A97: S . (i9 + 1) c= S . i9 by A47;
S . i9 in A ;
then ex Y99 being Subset of X st
( Y99 = S . i9 & card Y99 = omega ) ;
then consider Fa being Function of (the_subsets_of_card (n,((S . i9) \ {a9}))),k, Ha being Subset of ((S . i9) \ {a9}) such that
Ha is infinite and
Fa | (the_subsets_of_card (n,Ha)) is constant and
A98: for Y99 being Element of the_subsets_of_card (n,((S . i9) \ {a9})) holds Fa . Y99 = F . (Y99 \/ {a9}) by A7;
A99: { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 ) } c= S . (i9 + 1) by ;
now :: thesis: for x being object st x in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 )
}
holds
x in (S . i9) \ {(a . i9)}
let x be object ; :: thesis: ( x in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 )
}
implies x in (S . i9) \ {(a . i9)} )

assume x in { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 )
}
; :: thesis: x in (S . i9) \ {(a . i9)}
then A100: x in S . (i9 + 1) by A99;
then not x in {(a . i9)} by ;
hence x in (S . i9) \ {(a . i9)} by ; :: thesis: verum
end;
then { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 ) } c= (S . i9) \ {(a . i9)} ;
then the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 )
}
) c= the_subsets_of_card (n,((S . i9) \ {a9})) by Lm1;
then A101: Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 )
}
)
)
is Function of (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 )
}
)
)
,k by ;
A102: not card { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 )
}
c= card n by A86;
then not { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 ) } is empty ;
then A103: not the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 )
}
) is empty by ;
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 ;
then consider y being Element of k such that
A104: rng (Fa | (the_subsets_of_card (n, { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i9 )
}
)
)
)
= {y} by ;
reconsider y = y as set ;
take y ; :: thesis: ( y in k & S4[x,y] )
thus y in k by A6; :: thesis: S4[x,y]
for Y being set
for i being Element of NAT
for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
& ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds
ex l being Nat st
( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )
proof
reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
let Y be set ; :: thesis: for i being Element of NAT
for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
& ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds
ex l being Nat st
( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

let i be Element of NAT ; :: thesis: for Fi being Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k st i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
& ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) holds
ex l being Nat st
( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )

let Fi be Function of (the_subsets_of_card (n,((S . i) \ {(a . i)}))),k; :: thesis: ( i = x & Y = { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
& ( for Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fi . Y9 = F . (Y9 \/ {(a . i)}) ) implies ex l being Nat st
( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) )

assume A105: i = x ; :: thesis: ( not Y = { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
or ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ex l being Nat st
( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) )

k9 is Subset of NAT by STIRL2_1:8;
then reconsider l = y as Nat ;
assume A106: Y = { x9 where x9 is Element of omega : ex j being Element of NAT st
( a . j = x9 & j > i )
}
; :: thesis: ( ex Y9 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) st not Fi . Y9 = F . (Y9 \/ {(a . i)}) or ex l being Nat st
( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} ) )

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

take l ; :: thesis: ( l = y & l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )
thus l = y ; :: thesis: ( l in k & rng (Fi | (the_subsets_of_card (n,Y))) = {l} )
thus l in k by A6; :: thesis: rng (Fi | (the_subsets_of_card (n,Y))) = {l}
for x19 being Element of the_subsets_of_card (n,((S . i) \ {(a . i)})) holds Fa . x19 = Fi . x19
proof
let x19 be Element of the_subsets_of_card (n,((S . i) \ {(a . i)})); :: thesis: Fa . x19 = Fi . x19
thus Fa . x19 = F . (x19 \/ {(a . i)}) by
.= Fi . x19 by A107 ; :: thesis: verum
end;
hence rng (Fi | (the_subsets_of_card (n,Y))) = {l} by ; :: thesis: verum
end;
hence S4[x,y] ; :: thesis: verum
end;
consider g being sequence of k such that
A108: for x being object st x in NAT holds
S4[x,g . x] from g in Funcs (NAT,k) by ;
then ex g9 being Function st
( g = g9 & dom g9 = NAT & rng g9 c= k ) by FUNCT_2:def 2;
then consider k9 being object such that
k9 in rng g and
A109: g " {k9} is infinite by CARD_2:101;
set H = a .: (g " {k9});
g " {k9} c= dom g by RELAT_1:132;
then g " {k9},a .: (g " {k9}) are_equipotent by ;
then A110: card (g " {k9}) = card (a .: (g " {k9})) by CARD_1:5;
now :: thesis: for y being object st y in a .: (g " {k9}) holds
y in X
let y be object ; :: thesis: ( y in a .: (g " {k9}) implies y in X )
assume y in a .: (g " {k9}) ; :: thesis: y in X
then consider x being object such that
A111: [x,y] in a and
x in g " {k9} by RELAT_1:def 13;
x in dom a by ;
then reconsider i = x as Element of NAT ;
y = a . x by ;
then A112: y in S . i by A47;
S . i in the_subsets_of_card (omega,X) ;
hence y in X by A112; :: thesis: verum
end;
then reconsider H = a .: (g " {k9}) as Subset of X by TARSKI:def 3;
take H = H; :: thesis: ( H is infinite & F | (the_subsets_of_card ((n + 1),H)) is constant )
thus H is infinite by ; :: thesis: F | (the_subsets_of_card ((n + 1),H)) is constant
A113: for y being set st y in dom (F | (the_subsets_of_card ((n + 1),H))) holds
(F | (the_subsets_of_card ((n + 1),H))) . y = k9
proof
let y be set ; :: thesis: ( y in dom (F | (the_subsets_of_card ((n + 1),H))) implies (F | (the_subsets_of_card ((n + 1),H))) . y = k9 )
assume y in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis: (F | (the_subsets_of_card ((n + 1),H))) . y = k9
then A114: y in the_subsets_of_card ((n + 1),H) by RELAT_1:57;
then consider Y being Subset of H such that
A115: y = Y and
A116: card Y = n + 1 ;
set y0 = min* Y;
set Y9 = y \ {(min* Y)};
Y c= X by XBOOLE_1:1;
then A117: Y c= NAT by A5;
then A118: min* Y in Y by ;
then consider x0 being object such that
x0 in dom a and
A119: x0 in g " {k9} and
A120: min* Y = a . x0 by FUNCT_1:def 6;
consider y09 being object such that
y09 in rng g and
A121: [x0,y09] in g and
A122: y09 in {k9} by ;
A123: x0 in dom g by ;
A124: g . x0 = y09 by ;
reconsider x0 = x0 as Element of NAT by A123;
set Y0 = { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
;
{(min* Y)} c= y by ;
then A125: (y \ {(min* Y)}) \/ {(a . x0)} = y by ;
reconsider a9 = a . x0 as Element of S . x0 by A47;
S . x0 in the_subsets_of_card (omega,X) ;
then ex S0 being Subset of X st
( S0 = S . x0 & card S0 = omega ) ;
then consider F0 being Function of (the_subsets_of_card (n,((S . x0) \ {a9}))),k, H0 being Subset of ((S . x0) \ {a9}) such that
H0 is infinite and
F0 | (the_subsets_of_card (n,H0)) is constant and
A126: for Y9 being Element of the_subsets_of_card (n,((S . x0) \ {a9})) holds F0 . Y9 = F . (Y9 \/ {a9}) by A7;
reconsider y9 = y as finite set by ;
card (y \ {(min* Y)}) c= card y9 by CARD_1:11;
then reconsider Y99 = y \ {(min* Y)} as finite set ;
A127: { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 ) } c= S . (x0 + 1) by ;
now :: thesis: for x being object st x in y \ {(min* Y)} holds
x in { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
let x be object ; :: thesis: ( x in y \ {(min* Y)} implies x in { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
)

assume A128: x in y \ {(min* Y)} ; :: thesis: x in { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}

then A129: x in y ;
then consider j being object such that
A130: j in dom a and
j in g " {k9} and
A131: x = a . j by ;
reconsider x9 = x as Element of omega by ;
A132: not x in {(min* Y)} by ;
ex j being Element of NAT st
( a . j = x9 & j > x0 )
proof
reconsider j = j as Element of NAT by A130;
take j ; :: thesis: ( a . j = x9 & j > x0 )
thus a . j = x9 by A131; :: thesis: j > x0
A133: min* Y <= x9 by ;
thus j > x0 :: thesis: verum
proof
assume A134: x0 >= j ; :: thesis: contradiction
x0 <> j by ;
hence contradiction by A60, A120, A131, A133, A134; :: thesis: verum
end;
end;
hence x in { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
; :: thesis: verum
end;
then A135: y \ {(min* Y)} is Subset of { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
by TARSKI:def 3;
min* Y in {(min* Y)} by TARSKI:def 1;
then not a . x0 in y \ {(min* Y)} by ;
then card y9 = (card Y99) + 1 by ;
then A136: y \ {(min* Y)} in the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
) by ;
ex l being Nat st
( l = g . x0 & l in k & rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
)
)
)
= {l} ) by ;
then A137: rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
)
)
)
= {k9} by ;
S . (x0 + 1) c= S . x0 by A47;
then { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 ) } c= S . x0 by A127;
then A138: { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 ) } \ {(a . x0)} c= (S . x0) \ {(a . x0)} by XBOOLE_1:33;
not a . x0 in { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
by ;
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 ;
then A139: the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
) c= the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by Lm1;
then A140: y \ {(min* Y)} in the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by A136;
reconsider Y9 = y \ {(min* Y)} as Element of the_subsets_of_card (n,((S . x0) \ {(a . x0)})) by ;
Y9 in dom F0 by ;
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 ;
then (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
)
)
) . Y9 in rng (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
)
)
)
by FUNCT_1:3;
then (F0 | (the_subsets_of_card (n, { x where x is Element of omega : ex j being Element of NAT st
( a . j = x & j > x0 )
}
)
)
) . Y9 = k9 by ;
then A141: F0 . Y9 = k9 by ;
F0 . Y9 = F . (Y9 \/ {(a . x0)}) by A126;
hence (F | (the_subsets_of_card ((n + 1),H))) . y = k9 by ; :: thesis: verum
end;
for x, y being object st x in dom (F | (the_subsets_of_card ((n + 1),H))) & y in dom (F | (the_subsets_of_card ((n + 1),H))) holds
(F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y
proof
let x, y be object ; :: thesis: ( x in dom (F | (the_subsets_of_card ((n + 1),H))) & y in dom (F | (the_subsets_of_card ((n + 1),H))) implies (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y )
assume x in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis: ( not y in dom (F | (the_subsets_of_card ((n + 1),H))) or (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y )
then A142: (F | (the_subsets_of_card ((n + 1),H))) . x = k9 by A113;
assume y in dom (F | (the_subsets_of_card ((n + 1),H))) ; :: thesis: (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y
hence (F | (the_subsets_of_card ((n + 1),H))) . x = (F | (the_subsets_of_card ((n + 1),H))) . y by ; :: thesis: verum
end;
hence F | (the_subsets_of_card ((n + 1),H)) is constant by FUNCT_1:def 10; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
A143: S1[ 0 ]
proof
let k be Nat; :: thesis: for X being set
for F being Function of (),k st card X = omega & X c= omega & k <> 0 holds
ex H being Subset of X st
( H is infinite & F | () is constant )

let X be set ; :: thesis: for F being Function of (),k st card X = omega & X c= omega & k <> 0 holds
ex H being Subset of X st
( H is infinite & F | () is constant )

set H = X;
X c= X ;
then reconsider H = X as Subset of X ;
let F be Function of (),k; :: thesis: ( card X = omega & X c= omega & k <> 0 implies ex H being Subset of X st
( H is infinite & F | () is constant ) )

assume A144: card X = omega ; :: thesis: ( not X c= omega or not k <> 0 or ex H being Subset of X st
( H is infinite & F | () is constant ) )

assume X c= omega ; :: thesis: ( not k <> 0 or ex H being Subset of X st
( H is infinite & F | () is constant ) )

assume k <> 0 ; :: thesis: ex H being Subset of X st
( H is infinite & F | () is constant )

take H ; :: thesis: ( H is infinite & F | () is constant )
thus H is infinite by A144; :: thesis: F | () is constant
for x, y being object st x in dom (F | ()) & y in dom (F | ()) holds
(F | ()) . x = (F | ()) . y
proof
let x, y be object ; :: thesis: ( x in dom (F | ()) & y in dom (F | ()) implies (F | ()) . x = (F | ()) . y )
assume A145: x in dom (F | ()) ; :: thesis: ( not y in dom (F | ()) or (F | ()) . x = (F | ()) . y )
A146: dom (F | ()) = dom (F | ) by Lm2
.= (dom F) /\ by RELAT_1:61 ;
assume y in dom (F | ()) ; :: thesis: (F | ()) . x = (F | ()) . y
then y in by ;
then A147: y = 0 by TARSKI:def 1;
x in by ;
hence (F | ()) . x = (F | ()) . y by ; :: thesis: verum
end;
hence F | () is constant by FUNCT_1:def 10; :: thesis: verum
end;
for n being Nat holds S1[n] from hence for F being Function of (the_subsets_of_card (n,X)),k st card X = omega & X c= omega & k <> 0 holds
ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) ; :: thesis: verum