set D = the_subsets_of_card n,X;
reconsider D = the_subsets_of_card n,X as non empty set by A2, GROUP_10:2;
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 FUNCT_1:sch 4();
for y being set st y in rng IT holds
y in the_subsets_of_card n,Y
proof
let y be
set ;
( y in rng IT implies y in the_subsets_of_card n,Y )
assume
y in rng IT
;
y in the_subsets_of_card n,Y
then consider x being
set such that A5:
x in dom IT
and A6:
y = IT . x
by FUNCT_1:def 5;
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:11;
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:144;
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:60;
then
card y9 = n
by A7, A8, CARD_1:21;
hence
y in the_subsets_of_card n,
Y
;
verum
end;
then
rng IT c= the_subsets_of_card n,Y
by TARSKI:def 3;
then reconsider IT = IT as Function of (the_subsets_of_card n,X),(the_subsets_of_card n,Y) by A4, FUNCT_2:4;
take
IT
; 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; verum