let X, Y, z be set ; :: thesis: ( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z )
A1: dom (X --> (Y --> z)) = X by FUNCOP_1:13;
A2: dom (Y --> z) = Y by FUNCOP_1:13;
rng (Y --> z) c= {z} by FUNCOP_1:13;
then Y --> z in Funcs (Y,{z}) by A2, FUNCT_2:def 2;
then ( rng (X --> (Y --> z)) c= {(Y --> z)} & {(Y --> z)} c= Funcs (Y,{z}) ) by FUNCOP_1:13, ZFMISC_1:31;
then rng (X --> (Y --> z)) c= Funcs (Y,{z}) by XBOOLE_1:1;
then A3: dom (uncurry (X --> (Y --> z))) = [:X,Y:] by A1, FUNCT_5:26;

A4: now

let x be set ; :: thesis: ( x in [:X,Y:] implies (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x )
assume A5: x in [:X,Y:] ; :: thesis: (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x
then consider y1 being set , g being Function, y2 being set such that
A6: x = [y1,y2] and
A7: ( y1 in X & g = (X --> (Y --> z)) . y1 ) and
A8: y2 in dom g by A1, A3, FUNCT_5:def 2;
A9: g = Y --> z by A7, FUNCOP_1:7;
then (Y --> z) . y2 = z by A2, A8, FUNCOP_1:7;
then z = (uncurry (X --> (Y --> z))) . (y1,y2) by A1, A7, A8, A9, FUNCT_5:38;
hence (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x by A5, A6, FUNCOP_1:7; :: thesis: verum

end;

dom ([:X,Y:] --> z) = [:X,Y:] by FUNCOP_1:13;
hence uncurry (X --> (Y --> z)) = [:X,Y:] --> z by A3, A4, FUNCT_1:2; :: thesis: uncurry' (X --> (Y --> z)) = [:Y,X:] --> z
then ~ (uncurry (X --> (Y --> z))) = [:Y,X:] --> z by Th12;
hence uncurry' (X --> (Y --> z)) = [:Y,X:] --> z by FUNCT_5:def 4; :: thesis: verum