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:] & dom (X --> (Y --> z)) = X & dom (Y --> (X --> z)) = Y & dom (Y --> z) = Y & dom (X --> z) = X ) by FUNCOP_1:19;
then A3: ( dom (curry ([:X,Y:] --> z)) = X & dom (curry' ([:X,Y:] --> z)) = Y ) by A1, FUNCT_5:31;

now

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

now

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

end;

hence (curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x by A2, A5, A6, FUNCT_1:9; :: thesis: verum

end;

hence curry ([:X,Y:] --> z) = X --> (Y --> z) by A2, A3, FUNCT_1:9; :: thesis: curry' ([:X,Y:] --> z) = Y --> (X --> z)

now

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

now

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

end;

hence (curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x by A2, A8, A9, FUNCT_1:9; :: thesis: verum

end;

hence curry' ([:X,Y:] --> z) = Y --> (X --> z) by A2, A3, FUNCT_1:9; :: thesis: verum