let f be Function; :: thesis: ( curry f = curry' (~ f) & uncurry f = ~ (uncurry' f) )
A1: dom (curry (~ (~ f))) = proj1 (dom (~ (~ f))) by FUNCT_5:def 3;
A2: dom (curry f) = proj1 (dom f) by FUNCT_5:def 3;
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 set ; :: 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 set such that
A4: [x,y] in dom (~ (~ f)) by A1, RELAT_1:def 4;
[y,x] in dom (~ f) by A4, FUNCT_4:43;
then [x,y] in dom f by FUNCT_4:43;
hence x in dom (curry f) by A2, RELAT_1:def 4; :: thesis: verum

end;

let x be set ; :: 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 set such that
A5: [x,y] in dom f by A2, RELAT_1:def 4;
[y,x] in dom (~ f) by A5, FUNCT_4:43;
then [x,y] in dom (~ (~ f)) by FUNCT_4:43;
hence x in dom (curry (~ (~ f))) by A1, RELAT_1:def 4; :: thesis: verum

end;

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

now

let x be set ; :: 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
then reconsider g = (curry f) . x, h = (curry' (~ f)) . x as Function by A6, A3, FUNCT_5:37;
A8: dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) by A7, FUNCT_5:38;
A9: dom h = proj1 ((dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:]) by A6, A3, A7, FUNCT_5:41;
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 set ; :: 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 set such that
A11: [b,a] in (dom f) /\ [:{x},(proj2 (dom f)):] by A8, RELAT_1:def 5;
[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:107;
[b,a] in dom f by A11, XBOOLE_0:def 4;
then A13: [a,b] in dom (~ f) by FUNCT_4:43;
proj2 (dom f) = proj1 (dom (~ f)) by FUNCT_5:20;
then [a,b] in (dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:] by A13, A12, XBOOLE_0:def 4;
hence a in dom h by A9, RELAT_1:def 4; :: thesis: verum

end;

let a be set ; :: 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 set such that
A14: [a,b] in (dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:] by A9, RELAT_1:def 4;
[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:107;
[a,b] in dom (~ f) by A14, XBOOLE_0:def 4;
then A16: [b,a] in dom f by FUNCT_4:43;
proj2 (dom f) = proj1 (dom (~ f)) by FUNCT_5:20;
then [b,a] in (dom f) /\ [:{x},(proj2 (dom f)):] by A16, A15, XBOOLE_0:def 4;
hence a in dom g by A8, RELAT_1:def 5; :: thesis: verum

end;

now

let a be set ; :: 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:38;
h . a = (~ f) . a,x by A6, A3, A7, A10, A17, FUNCT_5:41;
hence g . a = h . a by A18, FUNCT_4:def 2; :: thesis: verum

end;

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

end;

hence curry f = curry' (~ f) by A6, A3, FUNCT_1:9; :: 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 set ; :: 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 set , g being Function, y being set such that
A21: a = [x,y] and
x in dom f and
g = f . x and
y in dom g by FUNCT_5:def 4;
[y,x] in dom (~ (uncurry f)) by A20, A21, FUNCT_4:43;
hence a in dom (~ (~ (uncurry f))) by A21, FUNCT_4:43; :: thesis: verum

end;

let a be set ; :: 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 set st
( a = [y,x] & [x,y] in dom (~ (uncurry f)) ) by FUNCT_4:def 2;
hence a in dom (uncurry f) by FUNCT_4:43; :: thesis: verum

end;

A22: now

let a be set ; :: 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 set 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:44, FUNCT_4:def 2;
hence (uncurry f) . a = (~ (~ (uncurry f))) . a by A23; :: thesis: verum

end;

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