let X, Y, Z be set ; :: thesis:
deffunc H₁( Function) -> Function = curry $1;
consider f being Function such that
A1: ( dom f = Funcs ([:X,Y:],Z) & ( for g being Function st g in Funcs ([:X,Y:],Z) holds
f . g = H₁(g) ) ) from FUNCT_5:sch 1();

A2: now :: thesis:

assume A3: [:X,Y:] <> {} ; :: thesis:
thus Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent :: thesis:

proof

take f ; :: according to WELLORD2:def 4 :: thesis:
thus f is one-to-one :: thesis:

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A4: x1 in dom f and
A5: x2 in dom f and
A6: f . x1 = f . x2 ; :: thesis:
consider g2 being Function such that
A7: x2 = g2 and
A8: dom g2 = [:X,Y:] and
rng g2 c= Z by A1, A5, FUNCT_2:def 2;
A9: f . x2 = curry g2 by A1, A5, A7;
consider g1 being Function such that
A10: x1 = g1 and
A11: dom g1 = [:X,Y:] and
rng g1 c= Z by A1, A4, FUNCT_2:def 2;
f . x1 = curry g1 by A1, A4, A10;
hence x1 = x2 by A6, A10, A11, A7, A8, A9, Th37; :: thesis:

end;

thus dom f = Funcs ([:X,Y:],Z) by A1; :: thesis:
thus rng f c= Funcs (X,(Funcs (Y,Z))) :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A12: x in dom f and
A13: y = f . x by FUNCT_1:def 3;
consider g being Function such that
A14: x = g and
A15: dom g = [:X,Y:] and
A16: rng g c= Z by A1, A12, FUNCT_2:def 2;
A17: dom (curry g) = X by A3, A15, Th17;
( rng (curry g) c= Funcs (Y,(rng g)) & Funcs (Y,(rng g)) c= Funcs (Y,Z) ) by A15, A16, Th28, Th49;
then A18: rng (curry g) c= Funcs (Y,Z) ;
y = curry g by A1, A12, A13, A14;
hence y in Funcs (X,(Funcs (Y,Z))) by A17, A18, FUNCT_2:def 2; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in Funcs (X,(Funcs (Y,Z))) ; :: thesis:
then consider g being Function such that
A19: y = g and
A20: dom g = X and
A21: rng g c= Funcs (Y,Z) by FUNCT_2:def 2;
( dom (uncurry g) = [:X,Y:] & rng (uncurry g) c= Z ) by A20, A21, Th19, Th34;
then A22: uncurry g in Funcs ([:X,Y:],Z) by FUNCT_2:def 2;
Y <> {} by A3, ZFMISC_1:90;
then curry (uncurry g) = g by A21, Th41;
then f . (uncurry g) = y by A1, A19, A22;
hence y in proj2 f by A1, A22, FUNCT_1:def 3; :: thesis:

end;

hence card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) by CARD_1:5; :: thesis:

end;

now :: thesis:

assume A23: [:X,Y:] = {} ; :: thesis:
then A24: Funcs ([:X,Y:],Z) = {{}} by Th50;

A25: now :: thesis:

assume Y = {} ; :: thesis:
then Funcs (Y,Z) = {{}} by Th50;
then Funcs (X,(Funcs (Y,Z))) = {(X --> {})} by Th52;
hence Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent by A24, CARD_1:28; :: thesis:

end;

( X = {} or Y = {} ) by A23;
hence Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent by A24, A25, Th50; :: thesis:
( X = {} implies Funcs (X,(Funcs (Y,Z))) = {{}} ) by Th50;
hence card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) by A23, A25, Th50, CARD_1:5; :: thesis:

end;

hence ( Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent & card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) ) by A2; :: thesis: