let X, Y, z be set ; :: thesis: ( [:X,Y:] <> {} implies ( curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z) ) )
assume A1: [:X,Y:] <> {} ; :: thesis: ( curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z) )
A2: dom ([:X,Y:] --> z) = [:X,Y:] by FUNCOP_1:13;
A3: dom (X --> z) = X by FUNCOP_1:13;

A4: now

let x be set ; :: thesis: ( x in Y implies (curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x )
assume A5: x in Y ; :: thesis: (curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x
then consider f being Function such that
A6: ( (curry' ([:X,Y:] --> z)) . x = f & dom f = X ) and
rng f c= rng ([:X,Y:] --> z) and
A7: for y being set st y in X holds
f . y = ([:X,Y:] --> z) . (y,x) by A1, A2, FUNCT_5:32;

A8: now

let y be set ; :: thesis: ( y in X implies f . y = (X --> z) . y )
assume A9: y in X ; :: thesis: f . y = (X --> z) . y
then A10: f . y = ([:X,Y:] --> z) . (y,x) by A7;
( (X --> z) . y = z & [y,x] in [:X,Y:] ) by A5, A9, FUNCOP_1:7, ZFMISC_1:87;
hence f . y = (X --> z) . y by A10, FUNCOP_1:7; :: thesis: verum

end;

(Y --> (X --> z)) . x = X --> z by A5, FUNCOP_1:7;
hence (curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x by A3, A6, A8, FUNCT_1:2; :: thesis: verum

end;

A11: dom (Y --> z) = Y by FUNCOP_1:13;

A12: now

let x be set ; :: thesis: ( x in X implies (curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x )
assume A13: x in X ; :: thesis: (curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x
then consider f being Function such that
A14: ( (curry ([:X,Y:] --> z)) . x = f & dom f = Y ) and
rng f c= rng ([:X,Y:] --> z) and
A15: for y being set st y in Y holds
f . y = ([:X,Y:] --> z) . (x,y) by A1, A2, FUNCT_5:29;

A16: now

let y be set ; :: thesis: ( y in Y implies f . y = (Y --> z) . y )
assume A17: y in Y ; :: thesis: f . y = (Y --> z) . y
then A18: f . y = ([:X,Y:] --> z) . (x,y) by A15;
( (Y --> z) . y = z & [x,y] in [:X,Y:] ) by A13, A17, FUNCOP_1:7, ZFMISC_1:87;
hence f . y = (Y --> z) . y by A18, FUNCOP_1:7; :: thesis: verum

end;

(X --> (Y --> z)) . x = Y --> z by A13, FUNCOP_1:7;
hence (curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x by A11, A14, A16, FUNCT_1:2; :: thesis: verum

end;

( dom (X --> (Y --> z)) = X & dom (curry ([:X,Y:] --> z)) = X ) by A1, A2, FUNCOP_1:13, FUNCT_5:24;
hence curry ([:X,Y:] --> z) = X --> (Y --> z) by A12, FUNCT_1:2; :: thesis: curry' ([:X,Y:] --> z) = Y --> (X --> z)
( dom (Y --> (X --> z)) = Y & dom (curry' ([:X,Y:] --> z)) = Y ) by A1, A2, FUNCOP_1:13, FUNCT_5:24;
hence curry' ([:X,Y:] --> z) = Y --> (X --> z) by A4, FUNCT_1:2; :: thesis: verum