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)
proof
let y be
object ;
( 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)))
;
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)
;
verum
end;
then
rng ((.: f) | (the_subsets_of_card (n,X))) c= 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; verum