let n, k be natural number ; :: thesis: for X being set
for F being Function of (the_subsets_of_card n,X),k st k <> 0 & not X is finite holds
ex H being Subset of X st
( not H is finite & 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 & not X is finite holds
ex H being Subset of X st
( not H is finite & F | (the_subsets_of_card n,H) is constant )
let F be Function of (the_subsets_of_card n,X),k; :: thesis: ( k <> 0 & not X is finite implies ex H being Subset of X st
( not H is finite & F | (the_subsets_of_card n,H) is constant ) )
assume that
A1: k <> 0 and
A2: not X is finite ; :: thesis: ex H being Subset of X st
( not H is finite & F | (the_subsets_of_card n,H) is constant )
F in Funcs (the_subsets_of_card n,X),k by A1, FUNCT_2:11;
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:104;
reconsider Y = Y as non empty set by A5;
Y, omega are_equipotent by A5, CARD_1:21, CARD_1:84;
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:3;
not card Y c= card n by A5;
then not the_subsets_of_card n,Y is empty by GROUP_10:2;
then f ||^ n in Funcs (the_subsets_of_card n,omega ),(the_subsets_of_card n,Y) by FUNCT_2:11;
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:46, XBOOLE_1:1;
A11: rng (F * (f ||^ n)) c= rng F by RELAT_1:45;
then A12: rng (F * (f ||^ n)) c= k by A3, XBOOLE_1:1;
reconsider F9 = F * (f ||^ n) as Function of (the_subsets_of_card n,omega ),k by A3, A10, A11, FUNCT_2:4, XBOOLE_1:1;
consider H9 being Subset of omega such that
A13: not H9 is finite and
A14: F9 | (the_subsets_of_card n,H9) is constant by A1, Lm4, CARD_1:84;
A15: rng (F9 | (the_subsets_of_card n,H9)) c= rng F9 by RELAT_1:99;
set H = f .: H9;
f .: H9 c= rng f by RELAT_1:144;
then reconsider H = f .: H9 as Subset of X by A4, A8, XBOOLE_1:1;
take H ; :: thesis: ( not H is finite & F | (the_subsets_of_card n,H) is constant )
H9,f .: H9 are_equipotent by A6, A7, CARD_1:60;
hence A16: not H is finite by A13, CARD_1:68; :: thesis: F | (the_subsets_of_card n,H) is constant
A17: rng (F | (the_subsets_of_card n,H)) c= rng F by RELAT_1:99;
dom (F9 | (the_subsets_of_card n,H9)) = the_subsets_of_card n,H9 by A10, Lm1, RELAT_1:91;
then F9 | (the_subsets_of_card n,H9) is Function of (the_subsets_of_card n,H9),k by A12, A15, FUNCT_2:4, XBOOLE_1:1;
then consider y being Element of k such that
A18: rng (F9 | (the_subsets_of_card n,H9)) = {y} by A1, A13, A14, FUNCT_2:188;
A19: not card omega c= card n ;
A20: 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:148
.= F .: ((f ||^ n) .: (the_subsets_of_card n,H9)) by A6, A19, Th1
.= F9 .: (the_subsets_of_card n,H9) by RELAT_1:159
.= {y} by A18, RELAT_1:148 ; :: thesis: verum

end;

dom (F | (the_subsets_of_card n,H)) = the_subsets_of_card n,H by A3, Lm1, RELAT_1:91;
then F | (the_subsets_of_card n,H) is Function of (the_subsets_of_card n,H),k by A3, A17, FUNCT_2:4, XBOOLE_1:1;
hence F | (the_subsets_of_card n,H) is constant by A1, A16, A20, FUNCT_2:188; :: thesis: verum