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 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 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 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 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 F' = 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 F' = F * (f ||^ n) as Function of the_subsets_of_card n,omega ,k by A3, A10, A11, FUNCT_2:4, XBOOLE_1:1;
consider H' being Subset of such that
A13: not H' is finite and
A14: F' | (the_subsets_of_card n,H') is constant by A1, Lm4, CARD_1:84;
A15: rng (F' | (the_subsets_of_card n,H')) c= rng F' by RELAT_1:99;
set H = f .: H';
f .: H' c= rng f by RELAT_1:144;
then reconsider H = f .: H' as Subset of by A4, A8, 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 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 (F' | (the_subsets_of_card n,H')) = the_subsets_of_card n,H' by A10, Lm1, RELAT_1:91;
then F' | (the_subsets_of_card n,H') is Function of the_subsets_of_card n,H',k by A12, A15, FUNCT_2:4, XBOOLE_1:1;
then consider y being Element of k such that
A18: rng (F' | (the_subsets_of_card n,H')) = {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,H')) by A6, A19, Th1
.= F' .: (the_subsets_of_card n,H') 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