let X, Y, Z be set ; :: thesis: ( Z in Funcs (X,Y) implies ( Z,X are_equipotent & card Z = card X ) )
assume Z in Funcs (X,Y) ; :: thesis: ( Z,X are_equipotent & card Z = card X )
then consider f being Function such that
A1: Z = f and
A2: dom f = X and
rng f c= Y by FUNCT_2:def 2;
thus Z,X are_equipotent :: thesis: card Z = card X

proof

consider g being Function such that
A3: ( dom g = Z & ( for x being object st x in Z holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3();
take g ; :: according to WELLORD2:def 4 :: thesis: ( g is one-to-one & proj1 g = Z & proj2 g = X )
thus g is one-to-one :: thesis: ( proj1 g = Z & proj2 g = X )

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 g or not y in proj1 g or not g . x = g . y or x = y )
assume that
A4: x in dom g and
A5: y in dom g ; :: thesis: ( not g . x = g . y or x = y )
A6: ( g . x = x `1 & g . y = y `1 ) by A3, A4, A5;
ex x1, x2 being object st [x1,x2] = y by A1, A3, A5, RELAT_1:def 1;
then A7: y = [(y `1),(y `2)] ;
ex x1, x2 being object st [x1,x2] = x by A1, A3, A4, RELAT_1:def 1;
then A8: x = [(x `1),(x `2)] ;
then x `2 = f . (x `1) by A1, A3, A4, FUNCT_1:1;
hence ( not g . x = g . y or x = y ) by A1, A3, A5, A8, A7, A6, FUNCT_1:1; :: thesis: verum

end;

thus dom g = Z by A3; :: thesis: proj2 g = X
thus rng g c= X :: according to XBOOLE_0:def 10 :: thesis: X c= proj2 g

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in X )
assume x in rng g ; :: thesis: x in X
then consider y being object such that
A9: y in dom g and
A10: x = g . y by FUNCT_1:def 3;
ex x1, x2 being object st [x1,x2] = y by A1, A3, A9, RELAT_1:def 1;
then A11: y = [(y `1),(y `2)] ;
x = y `1 by A3, A9, A10;
hence x in X by A1, A2, A3, A9, A11, FUNCT_1:1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in proj2 g )
assume x in X ; :: thesis: x in proj2 g
then A12: [x,(f . x)] in Z by A1, A2, FUNCT_1:def 2;
then g . [x,(f . x)] = [x,(f . x)] `1 by A3
.= x ;
hence x in proj2 g by A3, A12, FUNCT_1:def 3; :: thesis: verum

end;

hence card Z = card X by CARD_1:5; :: thesis: verum