let X, Y, Z be set ; :: thesis: ( Funcs [:X,Y:],Z, Funcs X,(Funcs Y,Z) are_equipotent & card (Funcs [:X,Y:],Z) = card (Funcs X,(Funcs Y,Z)) )
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

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

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = Funcs [:X,Y:],Z & proj2 f = Funcs X,(Funcs Y,Z) )
thus f is one-to-one :: thesis: ( proj1 f = Funcs [:X,Y:],Z & proj2 f = Funcs X,(Funcs Y,Z) )

proof

let x1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x1 in proj1 f or not b₁ in proj1 f or not f . x1 = f . b₁ or x1 = b₁ )
let x2 be set ; :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A4: x1 in dom f and
A5: x2 in dom f and
A6: f . x1 = f . x2 ; :: thesis: x1 = x2
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, Th51; :: thesis: verum

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Funcs X,(Funcs Y,Z) )
assume y in rng f ; :: thesis: y in Funcs X,(Funcs Y,Z)
then consider x being set such that
A12: x in dom f and
A13: y = f . x by FUNCT_1:def 5;
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, Th31;
( rng (curry g) c= Funcs Y,(rng g) & Funcs Y,(rng g) c= Funcs Y,Z ) by A15, A16, Th42, Th63;
then A18: rng (curry g) c= Funcs Y,Z by XBOOLE_1:1;
y = curry g by A1, A12, A13, A14;
hence y in Funcs X,(Funcs Y,Z) by A17, A18, FUNCT_2:def 2; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Funcs X,(Funcs Y,Z) or y in proj2 f )
assume y in Funcs X,(Funcs Y,Z) ; :: thesis: y in proj2 f
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, Th33, Th48;
then A22: uncurry g in Funcs [:X,Y:],Z by FUNCT_2:def 2;
Y <> {} by A3, ZFMISC_1:113;
then curry (uncurry g) = g by A21, Th55;
then f . (uncurry g) = y by A1, A19, A22;
hence y in proj2 f by A1, A22, FUNCT_1:def 5; :: thesis: verum

end;

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

end;

now

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

A25: now

assume Y = {} ; :: thesis: Funcs [:X,Y:],Z, Funcs X,(Funcs Y,Z) are_equipotent
then Funcs Y,Z = {{} } by Th64;
then Funcs X,(Funcs Y,Z) = {(X --> {} )} by Th66;
hence Funcs [:X,Y:],Z, Funcs X,(Funcs Y,Z) are_equipotent by A24, CARD_1:48; :: thesis: verum

end;

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

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: verum