let z be object ; :: thesis: for X, Y being set holds
( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z )
let X, Y be set ; :: thesis: ( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z )
A1: dom (X --> (Y --> z)) = X ;
A2: dom (Y --> z) = Y ;
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}) ;
then A3: dom (uncurry (X --> (Y --> z))) = [:X,Y:] by A1, FUNCT_5:26;

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

let x be object ; :: 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 object , g being Function, y2 being object 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 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;

thus uncurry (X --> (Y --> z)) = [:X,Y:] --> z by A3, A4; :: thesis: uncurry' (X --> (Y --> z)) = [:Y,X:] --> z
then ~ (uncurry (X --> (Y --> z))) = [:Y,X:] --> z by Th3;
hence uncurry' (X --> (Y --> z)) = [:Y,X:] --> z by FUNCT_5:def 4; :: thesis: verum