let f be Function; :: thesis: ( curry f = curry' (~ f) & uncurry f = ~ (uncurry' f) )
A1: ( curry' (~ f) = curry (~ (~ f)) & dom (curry f) = proj1 (dom f) & dom (curry (~ (~ f))) = proj1 (dom (~ (~ f))) ) by FUNCT_5:def 3, FUNCT_5:def 5;
A2: 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
A3: [x,y] in dom (~ (~ f)) by A1, RELAT_1:def 4;
[y,x] in dom (~ f) by A3, 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;

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 A1, RELAT_1:def 4; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom (curry f) implies (curry f) . x = (curry' (~ f)) . x )
assume A5: 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 A1, A2, FUNCT_5:37;
A6: ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds
g . y = f . x,y ) & dom h = proj1 ((dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:]) & ( for y being set st y in dom h holds
h . y = (~ f) . y,x ) ) by A1, A2, A5, FUNCT_5:38, FUNCT_5:41;
A7: 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
A8: [b,a] in (dom f) /\ [:{x},(proj2 (dom f)):] by A6, RELAT_1:def 5;
( [b,a] in dom f & [b,a] in [:{x},(proj2 (dom f)):] ) by A8, XBOOLE_0:def 4;
then ( [a,b] in dom (~ f) & [a,b] in [:(proj2 (dom f)),{x}:] & proj2 (dom f) = proj1 (dom (~ f)) ) by FUNCT_4:43, FUNCT_5:20, ZFMISC_1:107;
then [a,b] in (dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:] by XBOOLE_0:def 4;
hence a in dom h by A6, 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
A9: [a,b] in (dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:] by A6, RELAT_1:def 4;
( [a,b] in dom (~ f) & [a,b] in [:(proj1 (dom (~ f))),{x}:] ) by A9, XBOOLE_0:def 4;
then ( [b,a] in dom f & [b,a] in [:{x},(proj1 (dom (~ f))):] & proj2 (dom f) = proj1 (dom (~ f)) ) by FUNCT_4:43, FUNCT_5:20, ZFMISC_1:107;
then [b,a] in (dom f) /\ [:{x},(proj2 (dom f)):] by XBOOLE_0:def 4;
hence a in dom g by A6, RELAT_1:def 5; :: thesis: verum

end;

now

let a be set ; :: thesis: ( a in dom g implies g . a = h . a )
assume a in dom g ; :: thesis: g . a = h . a
then ( [x,a] in dom f & g . a = f . x,a & h . a = (~ f) . a,x ) by A1, A2, A5, A7, FUNCT_5:38, FUNCT_5:41;
hence g . a = h . a by FUNCT_4:def 2; :: thesis: verum

end;

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

end;

hence curry f = curry' (~ f) by A1, A2, FUNCT_1:9; :: thesis: uncurry f = ~ (uncurry' f)
A10: uncurry' f = ~ (uncurry f) by FUNCT_5:def 6;
A11: 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 A12: a in dom (uncurry f) ; :: thesis: a in dom (~ (~ (uncurry f)))
then consider x being set , g being Function, y being set such that
A13: ( a = [x,y] & x in dom f & g = f . x & y in dom g ) by FUNCT_5:def 4;
[y,x] in dom (~ (uncurry f)) by A12, A13, FUNCT_4:43;
hence a in dom (~ (~ (uncurry f))) by A13, 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;

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
A14: ( a = [y,x] & [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 A14, FUNCT_4:44, FUNCT_4:def 2;
hence (uncurry f) . a = (~ (~ (uncurry f))) . a by A14; :: thesis: verum

end;

hence uncurry f = ~ (uncurry' f) by A10, A11, FUNCT_1:9; :: thesis: verum