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 ) )
assume A1: dom f c= [:X,Y:] ; :: thesis: ( uncurry (curry f) = f & uncurry' (curry' f) = f )

A2: now :: thesis: for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
uncurry (curry f) = f

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 A3: dom f c= [:X,Y:] ; :: thesis: uncurry (curry f) = f
A4: 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 object ; :: 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 object ex g being Function ex z being object st
( x = [y,z] & y in dom (curry f) & g = (curry f) . y & z in dom g ) by Def2;
hence x in dom f by Th24; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in dom (uncurry (curry f)) )
assume A5: x in dom f ; :: thesis: x in dom (uncurry (curry f))
then A6: x = [(x `1),(x `2)] by A3, MCART_1:21;
then x `1 in dom (curry f) by A5, Th12;
then reconsider g = (curry f) . (x `1) as Function by FUNCOP_1:def 6;
( x `2 in dom g & x `1 in dom (curry f) ) by A5, A6, Th12, Th13;
hence x in dom (uncurry (curry f)) by A6, Th31; :: thesis: verum

end;

now :: thesis: for x being object st x in dom f holds
f . x = (uncurry (curry f)) . x

let x be object ; :: thesis: ( x in dom f implies f . x = (uncurry (curry f)) . x )
assume A7: x in dom f ; :: thesis: f . x = (uncurry (curry f)) . x
then A8: x = [(x `1),(x `2)] by A3, MCART_1:21;
then x `1 in dom (curry f) by A7, Th12;
then reconsider g = (curry f) . (x `1) as Function by FUNCOP_1:def 6;
(uncurry (curry f)) . x = g . (x `2) by A4, A7, Def2;
then f . ((x `1),(x `2)) = (uncurry (curry f)) . ((x `1),(x `2)) by A7, A8, Th13;
hence f . x = (uncurry (curry f)) . x by A8; :: thesis: verum

end;

hence uncurry (curry f) = f by A4; :: thesis: verum

end;

hence uncurry (curry f) = f by A1; :: thesis: uncurry' (curry' f) = f
dom (~ f) c= [:Y,X:] by A1, FUNCT_4:45;
then uncurry (curry (~ f)) = ~ f by A2;
hence uncurry' (curry' f) = f by A1, FUNCT_4:52; :: thesis: verum