let z be object ; :: thesis: for X, Y being set st [:X,Y:] <> {} holds
( curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z) )
let X, Y 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:] ;

A4: now :: thesis: for x being object st x in Y holds
(curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x

let x be object ; :: 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 object st y in X holds
f . y = ([:X,Y:] --> z) . (y,x) by A1, A2, FUNCT_5:32;

A8: now :: thesis: for y being object st y in X holds
f . y = (X --> z) . y

let y be object ; :: 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 A6, A8; :: thesis: verum

end;

A12: now :: thesis: for x being object st x in X holds
(curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x

let x be object ; :: 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 object st y in Y holds
f . y = ([:X,Y:] --> z) . (x,y) by A1, A2, FUNCT_5:29;

A16: now :: thesis: for y being object st y in Y holds
f . y = (Y --> z) . y

let y be object ; :: 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 A14, A16; :: thesis: verum

end;

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