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 A4: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then consider g1 being Function such that
A5: ( x1 = g1 & dom g1 = [:X,Y:] & rng g1 c= Z ) by A1, FUNCT_2:def 2;
consider g2 being Function such that
A6: ( x2 = g2 & dom g2 = [:X,Y:] & rng g2 c= Z ) by A1, A4, FUNCT_2:def 2;
( f . x1 = curry g1 & f . x2 = curry g2 ) by A1, A4, A5, A6;
hence x1 = x2 by A4, A5, A6, 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
A7: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
consider g being Function such that
A8: ( x = g & dom g = [:X,Y:] & rng g c= Z ) by A1, A7, FUNCT_2:def 2;
( rng (curry g) c= Funcs Y,(rng g) & Funcs Y,(rng g) c= Funcs Y,Z ) by A8, Th42, Th63;
then ( y = curry g & dom (curry g) = X & rng (curry g) c= Funcs Y,Z ) by A1, A3, A7, A8, Th31, XBOOLE_1:1;
hence y in Funcs X,(Funcs Y,Z) by 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
A9: ( y = g & dom g = X & rng g c= Funcs Y,Z ) by FUNCT_2:def 2;
( dom (uncurry g) = [:X,Y:] & rng (uncurry g) c= Z & Y <> {} ) by A3, A9, Th33, Th48, ZFMISC_1:113;
then A10: ( uncurry g in Funcs [:X,Y:],Z & curry (uncurry g) = g ) by A9, Th55, FUNCT_2:def 2;
then f . (uncurry g) = y by A1, A9;
hence y in proj2 f by A1, A10, 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 A11: [: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 A12: ( Funcs [:X,Y:],Z = {{} } & ( X = {} or Y = {} ) ) by Th64;
A13: ( X = {} implies Funcs X,(Funcs Y,Z) = {{} } ) by Th64;

A14: 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 A12, CARD_1:48; :: thesis: verum

end;

hence Funcs [:X,Y:],Z, Funcs X,(Funcs Y,Z) are_equipotent by A12, Th64; :: thesis: card (Funcs [:X,Y:],Z) = card (Funcs X,(Funcs Y,Z))
thus card (Funcs [:X,Y:],Z) = card (Funcs X,(Funcs Y,Z)) by A11, A13, A14, 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