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}

proof

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 F | (the_subsets_of_card (n,H)) is constant by A18; :: thesis: verum