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,Y:] & dom ([:Y,X:] --> z) = [:Y,X:] & dom (X --> (Y --> z)) = X & rng (X --> (Y --> z)) c= {(Y --> z)} & dom (Y --> z) = Y & rng (Y --> z) c= {z} ) by FUNCOP_1:19;
then Y --> z in Funcs Y,{z} by FUNCT_2:def 2;
then {(Y --> z)} c= Funcs Y,{z} by ZFMISC_1:37;
then rng (X --> (Y --> z)) c= Funcs Y,{z} by A1, XBOOLE_1:1;
then A2: ( dom (uncurry (X --> (Y --> z))) = [:X,Y:] & dom (uncurry' (X --> (Y --> z))) = [:Y,X:] ) by A1, FUNCT_5:33;

now

let x be set ; :: thesis: ( x in [:X,Y:] implies (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x )
assume A3: 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
A4: ( x = [y1,y2] & y1 in X & g = (X --> (Y --> z)) . y1 & y2 in dom g ) by A1, A2, FUNCT_5:def 4;
A5: g = Y --> z by A4, FUNCOP_1:13;
then (Y --> z) . y2 = z by A1, A4, FUNCOP_1:13;
then z = (uncurry (X --> (Y --> z))) . y1,y2 by A1, A4, A5, FUNCT_5:45;
hence (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x by A3, A4, FUNCOP_1:13; :: thesis: verum

end;

hence uncurry (X --> (Y --> z)) = [:X,Y:] --> z by A1, A2, FUNCT_1:9; :: 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 6; :: thesis: verum