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 A2, GROUP_10:1;

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 A3, FUNCT_2:def 1;

then A4: dom ((.: f) | (the_subsets_of_card (n,X))) = D by a1, a2, XBOOLE_1:28;

for y being object st y in rng ((.: f) | (the_subsets_of_card (n,X))) holds

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

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;

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 A3, FUNCT_2:def 1;

then A4: dom ((.: f) | (the_subsets_of_card (n,X))) = D by a1, a2, XBOOLE_1:28;

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

then
rng ((.: f) | (the_subsets_of_card (n,X))) c= the_subsets_of_card (n,Y)
;
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 B1, a1, a2, XBOOLE_1:28, A5;

Aa: x in the_subsets_of_card (n,X) ;

y = (.: f) . x by A6, A4, FUNCT_1:47;

then A8: y = f .: x by Aa, B1, FUNCT_3:def 1;

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;

card y9 = n by A7, A8, CARD_1:5, A1, A9, CARD_1:33;

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

end;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 B1, a1, a2, XBOOLE_1:28, A5;

Aa: x in the_subsets_of_card (n,X) ;

y = (.: f) . x by A6, A4, FUNCT_1:47;

then A8: y = f .: x by Aa, B1, FUNCT_3:def 1;

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;

card y9 = n by A7, A8, CARD_1:5, A1, A9, CARD_1:33;

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

hence (.: f) | (the_subsets_of_card (n,X)) is Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) by A4, FUNCT_2:2; :: thesis: verum