let X, Y be set ; :: thesis: for f being Function st dom f c= [:X,Y:] holds
( uncurry (curry f) = f & uncurry' (curry' f) = f )
let f be Function; :: thesis: ( dom f c= [:X,Y:] implies ( uncurry (curry f) = f & uncurry' (curry' f) = f ) )

A1: now

let X, Y be set ; :: thesis: for f being Function st dom f c= [:X,Y:] holds
uncurry (curry f) = f
let f be Function; :: thesis: ( dom f c= [:X,Y:] implies uncurry (curry f) = f )
assume A2: dom f c= [:X,Y:] ; :: thesis: uncurry (curry f) = f
A3: dom (uncurry (curry f)) = dom f

proof

thus dom (uncurry (curry f)) c= dom f :: according to XBOOLE_0:def 10 :: thesis: dom f c= dom (uncurry (curry f))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (uncurry (curry f)) or x in dom f )
assume x in dom (uncurry (curry f)) ; :: thesis: x in dom f
then ex y being set ex g being Function ex z being set st
( x = [y,z] & y in dom (curry f) & g = (curry f) . y & z in dom g ) by Def4;
hence x in dom f by Th38; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in dom (uncurry (curry f)) )
assume A4: x in dom f ; :: thesis: x in dom (uncurry (curry f))
then A5: x = [(x `1 ),(x `2 )] by A2, MCART_1:23;
then reconsider g = (curry f) . (x `1 ) as Function by A4, Th26;
( x `2 in dom g & x `1 in dom (curry f) ) by A4, A5, Th26, Th27;
hence x in dom (uncurry (curry f)) by A5, Th45; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom f implies f . x = (uncurry (curry f)) . x )
assume A6: x in dom f ; :: thesis: f . x = (uncurry (curry f)) . x
then A7: x = [(x `1 ),(x `2 )] by A2, MCART_1:23;
then reconsider g = (curry f) . (x `1 ) as Function by A6, Th26;
(uncurry (curry f)) . x = g . (x `2 ) by A3, A6, Def4;
then f . (x `1 ),(x `2 ) = (uncurry (curry f)) . (x `1 ),(x `2 ) by A6, A7, Th27;
hence f . x = (uncurry (curry f)) . x by A7; :: thesis: verum

end;

hence uncurry (curry f) = f by A3, FUNCT_1:9; :: thesis: verum

end;

assume A8: dom f c= [:X,Y:] ; :: thesis: ( uncurry (curry f) = f & uncurry' (curry' f) = f )
hence uncurry (curry f) = f by A1; :: thesis: uncurry' (curry' f) = f
dom (~ f) c= [:Y,X:] by A8, FUNCT_4:46;
then uncurry (curry (~ f)) = ~ f by A1;
hence uncurry' (curry' f) = f by A8, FUNCT_4:53; :: thesis: verum