set D = the_subsets_of_card (n,X);
reconsider D = the_subsets_of_card (n,X) as non empty set by ;
deffunc H1( set ) -> set = f .: \$1;
consider IT being Function such that
A4: ( dom IT = D & ( for x being Element of D holds IT . x = H1(x) ) ) from for y being object st y in rng IT holds
y in the_subsets_of_card (n,Y)
proof
let y be object ; :: thesis: ( y in rng IT implies y in the_subsets_of_card (n,Y) )
assume y in rng IT ; :: thesis: y in the_subsets_of_card (n,Y)
then consider x being object such that
A5: x in dom IT and
A6: y = IT . 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 A4, A5;
A8: y = f .: x by A4, A6;
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 ;
x,f .: x are_equipotent by ;
then card y9 = n by ;
hence y in the_subsets_of_card (n,Y) ; :: thesis: verum
end;
then rng IT c= the_subsets_of_card (n,Y) ;
then reconsider IT = IT as Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) by ;
take IT ; :: thesis: for x being Element of the_subsets_of_card (n,X) holds IT . x = f .: x
thus for x being Element of the_subsets_of_card (n,X) holds IT . x = f .: x by A4; :: thesis: verum