set IT = (.: f) | (the_subsets_of_card (n,X));
set D = the_subsets_of_card (n,X);
reconsider D = the_subsets_of_card (n,X) as non empty set by ;
a1: dom (.: f) = bool (dom f) by FUNCT_3:def 1;
a2: dom ((.: f) | (the_subsets_of_card (n,X))) = (dom (.: f)) /\ (the_subsets_of_card (n,X)) by RELAT_1:61;
B1: dom f = X by ;
then A4: dom ((.: f) | (the_subsets_of_card (n,X))) = D by ;
for y being object st y in rng ((.: f) | (the_subsets_of_card (n,X))) holds
y in the_subsets_of_card (n,Y)
proof
let y be object ; :: thesis: ( y in rng ((.: f) | (the_subsets_of_card (n,X))) implies y in the_subsets_of_card (n,Y) )
assume y in rng ((.: f) | (the_subsets_of_card (n,X))) ; :: thesis: y in the_subsets_of_card (n,Y)
then consider x being object such that
A5: x in dom ((.: f) | (the_subsets_of_card (n,X))) and
A6: y = ((.: f) | (the_subsets_of_card (n,X))) . x by FUNCT_1:def 3;
A7: ex x9 being Subset of X st
( x = x9 & card x9 = n ) by A4, A5;
reconsider x = x as Element of D by ;
Aa: x in the_subsets_of_card (n,X) ;
y = (.: f) . x by ;
then A8: y = f .: x by ;
f in Funcs (X,Y) by ;
then A9: ex f9 being Function st
( f = f9 & dom f9 = X & rng f9 c= Y ) by FUNCT_2:def 2;
f .: x c= rng f by RELAT_1:111;
then reconsider y9 = y as Subset of Y by ;
card y9 = n by ;
hence y in the_subsets_of_card (n,Y) ; :: thesis: verum
end;
then rng ((.: f) | (the_subsets_of_card (n,X))) c= the_subsets_of_card (n,Y) ;
hence (.: f) | (the_subsets_of_card (n,X)) is Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) by ; :: thesis: verum