theorem :: FUNCT_6:6

for z being object
for X, Y being set holds
( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z )