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 A1: ( k <> 0 & 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 )
consider Y being set such that
A2: ( Y c= X & card Y = omega ) by A1, CARD_3:104;
reconsider Y = Y as non empty set by A2;
Y, omega are_equipotent by A2, CARD_1:21, CARD_1:84;
then consider f being Function such that
A3: ( f is one-to-one & dom f = omega & rng f = Y ) by WELLORD2:def 4;
reconsider f = f as Function of omega ,Y by A3, FUNCT_2:3;
set F' = F * (f ||^ n);
F in Funcs (the_subsets_of_card n,X),k by A1, FUNCT_2:11;
then consider g1 being Function such that
A4: ( F = g1 & dom g1 = the_subsets_of_card n,X & rng g1 c= k ) by FUNCT_2:def 2;
not card omega c= card n ;
then A5: card n c= card omega ;
not card Y c= card n by A2;
then card n c= card Y ;
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 consider g2 being Function such that
A6: ( 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;
the_subsets_of_card n,Y c= the_subsets_of_card n,X by A2, Lm1;
then A7: dom (F * (f ||^ n)) = the_subsets_of_card n,omega by A6, A4, RELAT_1:46, XBOOLE_1:1;
A8: rng (F * (f ||^ n)) c= rng F by RELAT_1:45;
then A9: rng (F * (f ||^ n)) c= k by A4, XBOOLE_1:1;
reconsider F' = F * (f ||^ n) as Function of (the_subsets_of_card n,omega ),k by A8, A7, A4, FUNCT_2:4, XBOOLE_1:1;
consider H' being Subset of omega such that
A10: ( not H' is finite & F' | (the_subsets_of_card n,H') is constant ) by A1, Lm5, CARD_1:84;
A12: dom (F' | (the_subsets_of_card n,H')) = the_subsets_of_card n,H' by A7, Lm1, RELAT_1:91;
rng (F' | (the_subsets_of_card n,H')) c= rng F' by RELAT_1:99;
then F' | (the_subsets_of_card n,H') is Function of (the_subsets_of_card n,H'),k by A12, A9, FUNCT_2:4, XBOOLE_1:1;
then consider y being Element of k such that
A13: rng (F' | (the_subsets_of_card n,H')) = {y} by A10, A1, FUNCT_2:188;
set H = f .: H';
A14: f .: H' c= rng f by RELAT_1:144;
reconsider H = f .: H' as Subset of X by A2, A3, A14, XBOOLE_1:1;
take H ; :: thesis: ( not H is finite & F | (the_subsets_of_card n,H) is constant )
H',f .: H' are_equipotent by A3, CARD_1:60;
hence A15: not H is finite by A10, CARD_1:68; :: thesis: F | (the_subsets_of_card n,H) is constant
A17: dom (F | (the_subsets_of_card n,H)) = the_subsets_of_card n,H by Lm1, A4, RELAT_1:91;
rng (F | (the_subsets_of_card n,H)) c= rng F by RELAT_1:99;
then A18: F | (the_subsets_of_card n,H) is Function of (the_subsets_of_card n,H),k by A17, A4, FUNCT_2:4, XBOOLE_1:1;
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,H')) by A3, A5, Th1
.= F' .: (the_subsets_of_card n,H') by RELAT_1:159
.= {y} by A13, RELAT_1:148 ; :: thesis: verum

end;

hence F | (the_subsets_of_card n,H) is constant by A15, A1, A18, FUNCT_2:188; :: thesis: verum