let f be Function; :: thesis: ( curry f = curry' (~ f) & uncurry f = ~ (uncurry' f) )
A1: dom (curry (~ (~ f))) = proj1 (dom (~ (~ f))) by FUNCT_5:def 1;
A2: dom (curry f) = proj1 (dom f) by FUNCT_5:def 1;
A3: dom (curry (~ (~ f))) = dom (curry f)

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (curry (~ (~ f))) or x in dom (curry f) )
assume x in dom (curry (~ (~ f))) ; :: thesis: x in dom (curry f)
then consider y being object such that
A4: [x,y] in dom (~ (~ f)) by A1, XTUPLE_0:def 12;
[y,x] in dom (~ f) by A4, FUNCT_4:42;
then [x,y] in dom f by FUNCT_4:42;
hence x in dom (curry f) by A2, XTUPLE_0:def 12; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (curry f) or x in dom (curry (~ (~ f))) )
assume x in dom (curry f) ; :: thesis: x in dom (curry (~ (~ f)))
then consider y being object such that
A5: [x,y] in dom f by A2, XTUPLE_0:def 12;
[y,x] in dom (~ f) by A5, FUNCT_4:42;
then [x,y] in dom (~ (~ f)) by FUNCT_4:42;
hence x in dom (curry (~ (~ f))) by A1, XTUPLE_0:def 12; :: thesis: verum

end;

A6: curry' (~ f) = curry (~ (~ f)) by FUNCT_5:def 3;

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

let x be object ; :: thesis: ( x in dom (curry f) implies (curry f) . x = (curry' (~ f)) . x )
assume A7: x in dom (curry f) ; :: thesis: (curry f) . x = (curry' (~ f)) . x
reconsider g = (curry f) . x, h = (curry' (~ f)) . x as Function ;
A8: dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) by A7, FUNCT_5:31;
A9: dom h = proj1 ((dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:]) by A6, A3, A7, FUNCT_5:34;
A10: dom g = dom h

proof

thus dom g c= dom h :: according to XBOOLE_0:def 10 :: thesis: dom h c= dom g

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom g or a in dom h )
assume a in dom g ; :: thesis: a in dom h
then consider b being object such that
A11: [b,a] in (dom f) /\ [:{x},(proj2 (dom f)):] by A8, XTUPLE_0:def 13;
[b,a] in [:{x},(proj2 (dom f)):] by A11, XBOOLE_0:def 4;
then A12: [a,b] in [:(proj2 (dom f)),{x}:] by ZFMISC_1:88;
[b,a] in dom f by A11, XBOOLE_0:def 4;
then A13: [a,b] in dom (~ f) by FUNCT_4:42;
proj2 (dom f) = proj1 (dom (~ f)) by FUNCT_5:17;
then [a,b] in (dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:] by A13, A12, XBOOLE_0:def 4;
hence a in dom h by A9, XTUPLE_0:def 12; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom h or a in dom g )
assume a in dom h ; :: thesis: a in dom g
then consider b being object such that
A14: [a,b] in (dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:] by A9, XTUPLE_0:def 12;
[a,b] in [:(proj1 (dom (~ f))),{x}:] by A14, XBOOLE_0:def 4;
then A15: [b,a] in [:{x},(proj1 (dom (~ f))):] by ZFMISC_1:88;
[a,b] in dom (~ f) by A14, XBOOLE_0:def 4;
then A16: [b,a] in dom f by FUNCT_4:42;
proj2 (dom f) = proj1 (dom (~ f)) by FUNCT_5:17;
then [b,a] in (dom f) /\ [:{x},(proj2 (dom f)):] by A16, A15, XBOOLE_0:def 4;
hence a in dom g by A8, XTUPLE_0:def 13; :: thesis: verum

end;

now :: thesis: for a being object st a in dom g holds
g . a = h . a

let a be object ; :: thesis: ( a in dom g implies g . a = h . a )
assume A17: a in dom g ; :: thesis: g . a = h . a
then A18: ( [x,a] in dom f & g . a = f . (x,a) ) by A7, FUNCT_5:31;
h . a = (~ f) . (a,x) by A6, A3, A7, A10, A17, FUNCT_5:34;
hence g . a = h . a by A18, FUNCT_4:def 2; :: thesis: verum

end;

hence (curry f) . x = (curry' (~ f)) . x by A10; :: thesis: verum

end;

hence curry f = curry' (~ f) by A6, A3; :: thesis: uncurry f = ~ (uncurry' f)
A19: dom (uncurry f) = dom (~ (~ (uncurry f)))

proof

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom (uncurry f) or a in dom (~ (~ (uncurry f))) )
assume A20: a in dom (uncurry f) ; :: thesis: a in dom (~ (~ (uncurry f)))
then consider x being object , g being Function, y being object such that
A21: a = [x,y] and
x in dom f and
g = f . x and
y in dom g by FUNCT_5:def 2;
[y,x] in dom (~ (uncurry f)) by A20, A21, FUNCT_4:42;
hence a in dom (~ (~ (uncurry f))) by A21, FUNCT_4:42; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom (~ (~ (uncurry f))) or a in dom (uncurry f) )
assume a in dom (~ (~ (uncurry f))) ; :: thesis: a in dom (uncurry f)
then ex x, y being object st
( a = [y,x] & [x,y] in dom (~ (uncurry f)) ) by FUNCT_4:def 2;
hence a in dom (uncurry f) by FUNCT_4:42; :: thesis: verum

end;

A22: now :: thesis: for a being object st a in dom (~ (~ (uncurry f))) holds
(uncurry f) . a = (~ (~ (uncurry f))) . a

let a be object ; :: thesis: ( a in dom (~ (~ (uncurry f))) implies (uncurry f) . a = (~ (~ (uncurry f))) . a )
assume a in dom (~ (~ (uncurry f))) ; :: thesis: (uncurry f) . a = (~ (~ (uncurry f))) . a
then consider x, y being object such that
A23: a = [y,x] and
A24: [x,y] in dom (~ (uncurry f)) by FUNCT_4:def 2;
( (~ (uncurry f)) . (x,y) = (uncurry f) . (y,x) & (~ (uncurry f)) . (x,y) = (~ (~ (uncurry f))) . (y,x) ) by A24, FUNCT_4:43, FUNCT_4:def 2;
hence (uncurry f) . a = (~ (~ (uncurry f))) . a by A23; :: thesis: verum

end;

uncurry' f = ~ (uncurry f) by FUNCT_5:def 4;
hence uncurry f = ~ (uncurry' f) by A19, A22; :: thesis: verum