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 ;
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 ;
reconsider Y = Y as non empty set by A5;
Y, omega are_equipotent by ;
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 ;
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,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 ;
then A10: dom (F * (f ||^ n)) = the_subsets_of_card (n,omega) by ;
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 (),k by ;
consider H9 being Subset of omega such that
A13: H9 is infinite and
A14: F9 | (the_subsets_of_card (n,H9)) is constant by ;
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 ;
take H ; :: thesis: ( H is infinite & F | (the_subsets_of_card (n,H)) is constant )
H9,f .: H9 are_equipotent by ;
hence H is infinite by ; :: 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 ;
then F9 | (the_subsets_of_card (n,H9)) is Function of (the_subsets_of_card (n,H9)),k by ;
then consider y being Element of k such that
A16: rng (F9 | (the_subsets_of_card (n,H9))) = {y} by ;
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 ; :: thesis: verum
end;
thus F | (the_subsets_of_card (n,H)) is constant by A18; :: thesis: verum