let n, k be Nat; :: thesis: for X being set

for F being Function of (the_subsets_of_card (n,X)),k st k <> 0 & X is infinite 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 k <> 0 & X is infinite holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

let F be Function of (the_subsets_of_card (n,X)),k; :: thesis: ( k <> 0 & X is infinite implies ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) )

assume that

A1: k <> 0 and

A2: X is infinite ; :: thesis: ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

F in Funcs ((the_subsets_of_card (n,X)),k) by A1, FUNCT_2:8;

then A3: ex g1 being Function st

( F = g1 & dom g1 = the_subsets_of_card (n,X) & rng g1 c= k ) by FUNCT_2:def 2;

consider Y being set such that

A4: Y c= X and

A5: card Y = omega by A2, CARD_3:87;

reconsider Y = Y as non empty set by A5;

Y, omega are_equipotent by A5, CARD_1:5, CARD_1:47;

then consider f being Function such that

A6: f is one-to-one and

A7: dom f = omega and

A8: rng f = Y by WELLORD2:def 4;

reconsider f = f as Function of omega,Y by A7, A8, FUNCT_2:1;

not card Y c= card n by A5;

then not the_subsets_of_card (n,Y) is empty by GROUP_10:1;

then f ||^ n in Funcs ((the_subsets_of_card (n,omega)),(the_subsets_of_card (n,Y))) by FUNCT_2:8;

then A9: ex g2 being Function st

( f ||^ n = g2 & dom g2 = the_subsets_of_card (n,omega) & rng g2 c= the_subsets_of_card (n,Y) ) by FUNCT_2:def 2;

set F9 = F * (f ||^ n);

the_subsets_of_card (n,Y) c= the_subsets_of_card (n,X) by A4, Lm1;

then A10: dom (F * (f ||^ n)) = the_subsets_of_card (n,omega) by A3, A9, RELAT_1:27, XBOOLE_1:1;

A11: rng (F * (f ||^ n)) c= rng F by RELAT_1:26;

then A12: rng (F * (f ||^ n)) c= k by A3;

reconsider F9 = F * (f ||^ n) as Function of (the_subsets_of_card (n,omega)),k by A3, A10, A11, FUNCT_2:2, XBOOLE_1:1;

consider H9 being Subset of omega such that

A13: H9 is infinite and

A14: F9 | (the_subsets_of_card (n,H9)) is constant by A1, Lm4, CARD_1:47;

A15: rng (F9 | (the_subsets_of_card (n,H9))) c= rng F9 by RELAT_1:70;

set H = f .: H9;

f .: H9 c= rng f by RELAT_1:111;

then reconsider H = f .: H9 as Subset of X by A4, A8, XBOOLE_1:1;

take H ; :: thesis: ( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

H9,f .: H9 are_equipotent by A6, A7, CARD_1:33;

hence H is infinite by A13, CARD_1:38; :: thesis: F | (the_subsets_of_card (n,H)) is constant

dom (F9 | (the_subsets_of_card (n,H9))) = the_subsets_of_card (n,H9) by A10, Lm1, RELAT_1:62;

then F9 | (the_subsets_of_card (n,H9)) is Function of (the_subsets_of_card (n,H9)),k by A12, A15, FUNCT_2:2, XBOOLE_1:1;

then consider y being Element of k such that

A16: rng (F9 | (the_subsets_of_card (n,H9))) = {y} by A1, A13, A14, FUNCT_2:111;

A17: not card omega c= card n ;

A18: ex y being Element of k st rng (F | (the_subsets_of_card (n,H))) = {y}

for F being Function of (the_subsets_of_card (n,X)),k st k <> 0 & X is infinite 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 k <> 0 & X is infinite holds

ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

let F be Function of (the_subsets_of_card (n,X)),k; :: thesis: ( k <> 0 & X is infinite implies ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant ) )

assume that

A1: k <> 0 and

A2: X is infinite ; :: thesis: ex H being Subset of X st

( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

F in Funcs ((the_subsets_of_card (n,X)),k) by A1, FUNCT_2:8;

then A3: ex g1 being Function st

( F = g1 & dom g1 = the_subsets_of_card (n,X) & rng g1 c= k ) by FUNCT_2:def 2;

consider Y being set such that

A4: Y c= X and

A5: card Y = omega by A2, CARD_3:87;

reconsider Y = Y as non empty set by A5;

Y, omega are_equipotent by A5, CARD_1:5, CARD_1:47;

then consider f being Function such that

A6: f is one-to-one and

A7: dom f = omega and

A8: rng f = Y by WELLORD2:def 4;

reconsider f = f as Function of omega,Y by A7, A8, FUNCT_2:1;

not card Y c= card n by A5;

then not the_subsets_of_card (n,Y) is empty by GROUP_10:1;

then f ||^ n in Funcs ((the_subsets_of_card (n,omega)),(the_subsets_of_card (n,Y))) by FUNCT_2:8;

then A9: ex g2 being Function st

( f ||^ n = g2 & dom g2 = the_subsets_of_card (n,omega) & rng g2 c= the_subsets_of_card (n,Y) ) by FUNCT_2:def 2;

set F9 = F * (f ||^ n);

the_subsets_of_card (n,Y) c= the_subsets_of_card (n,X) by A4, Lm1;

then A10: dom (F * (f ||^ n)) = the_subsets_of_card (n,omega) by A3, A9, RELAT_1:27, XBOOLE_1:1;

A11: rng (F * (f ||^ n)) c= rng F by RELAT_1:26;

then A12: rng (F * (f ||^ n)) c= k by A3;

reconsider F9 = F * (f ||^ n) as Function of (the_subsets_of_card (n,omega)),k by A3, A10, A11, FUNCT_2:2, XBOOLE_1:1;

consider H9 being Subset of omega such that

A13: H9 is infinite and

A14: F9 | (the_subsets_of_card (n,H9)) is constant by A1, Lm4, CARD_1:47;

A15: rng (F9 | (the_subsets_of_card (n,H9))) c= rng F9 by RELAT_1:70;

set H = f .: H9;

f .: H9 c= rng f by RELAT_1:111;

then reconsider H = f .: H9 as Subset of X by A4, A8, XBOOLE_1:1;

take H ; :: thesis: ( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

H9,f .: H9 are_equipotent by A6, A7, CARD_1:33;

hence H is infinite by A13, CARD_1:38; :: thesis: F | (the_subsets_of_card (n,H)) is constant

dom (F9 | (the_subsets_of_card (n,H9))) = the_subsets_of_card (n,H9) by A10, Lm1, RELAT_1:62;

then F9 | (the_subsets_of_card (n,H9)) is Function of (the_subsets_of_card (n,H9)),k by A12, A15, FUNCT_2:2, XBOOLE_1:1;

then consider y being Element of k such that

A16: rng (F9 | (the_subsets_of_card (n,H9))) = {y} by A1, A13, A14, FUNCT_2:111;

A17: not card omega c= card n ;

A18: ex y being Element of k st rng (F | (the_subsets_of_card (n,H))) = {y}

proof

thus
F | (the_subsets_of_card (n,H)) is constant
by A18; :: thesis: verum
take
y
; :: thesis: rng (F | (the_subsets_of_card (n,H))) = {y}

thus rng (F | (the_subsets_of_card (n,H))) = F .: (the_subsets_of_card (n,H)) by RELAT_1:115

.= F .: ((f ||^ n) .: (the_subsets_of_card (n,H9))) by A6, A17, Th1

.= F9 .: (the_subsets_of_card (n,H9)) by RELAT_1:126

.= {y} by A16, RELAT_1:115 ; :: thesis: verum

end;thus rng (F | (the_subsets_of_card (n,H))) = F .: (the_subsets_of_card (n,H)) by RELAT_1:115

.= F .: ((f ||^ n) .: (the_subsets_of_card (n,H9))) by A6, A17, Th1

.= F9 .: (the_subsets_of_card (n,H9)) by RELAT_1:126

.= {y} by A16, RELAT_1:115 ; :: thesis: verum