set D = the_subsets_of_card (n,X);

reconsider D = the_subsets_of_card (n,X) as non empty set by A2, GROUP_10:1;

deffunc H_{1}( set ) -> set = f .: $1;

consider IT being Function such that

A4: ( dom IT = D & ( for x being Element of D holds IT . x = H_{1}(x) ) )
from FUNCT_1:sch 4();

for y being object st y in rng IT holds

y in 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 A4, FUNCT_2:2;

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

reconsider D = the_subsets_of_card (n,X) as non empty set by A2, GROUP_10:1;

deffunc H

consider IT being Function such that

A4: ( dom IT = D & ( for x being Element of D holds IT . x = H

for y being object st y in rng IT holds

y in the_subsets_of_card (n,Y)

proof

then
rng IT c= the_subsets_of_card (n,Y)
;
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 A3, FUNCT_2:8;

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 A8, A9, XBOOLE_1:1;

x,f .: x are_equipotent by A1, A4, A5, A9, CARD_1:33;

then card y9 = n by A7, A8, CARD_1:5;

hence y in the_subsets_of_card (n,Y) ; :: thesis: verum

end;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 A3, FUNCT_2:8;

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 A8, A9, XBOOLE_1:1;

x,f .: x are_equipotent by A1, A4, A5, A9, CARD_1:33;

then card y9 = n by A7, A8, CARD_1:5;

hence y in the_subsets_of_card (n,Y) ; :: thesis: verum

then reconsider IT = IT as Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) by A4, FUNCT_2:2;

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