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 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 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)
;
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:2;
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