let z be object ; 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 ; ( 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 for x being object st x in [:X,Y:] holds
(uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . xlet x be
object ;
( x in [:X,Y:] implies (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x )assume A5:
x in [:X,Y:]
;
(uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . xthen 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;
verum end;
thus
uncurry (X --> (Y --> z)) = [:X,Y:] --> z
by A3, A4; 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; verum