let f, g be Function; for x, y being object st [x,y] in dom f & g = (curry f) . x holds
( y in dom g & g . y = f . (x,y) )
let x, y be object ; ( [x,y] in dom f & g = (curry f) . x implies ( y in dom g & g . y = f . (x,y) ) )
assume that
A1:
[x,y] in dom f
and
A2:
g = (curry f) . x
; ( y in dom g & g . y = f . (x,y) )
x in proj1 (dom f)
by A1, XTUPLE_0:def 12;
then A3:
ex h being Function st
( (curry f) . x = h & dom h = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom h holds
h . y = f . (x,y) ) )
by Def1;
y in proj2 (dom f)
by A1, XTUPLE_0:def 13;
then
[x,y] in [:{x},(proj2 (dom f)):]
by ZFMISC_1:105;
then
[x,y] in (dom f) /\ [:{x},(proj2 (dom f)):]
by A1, XBOOLE_0:def 4;
hence
y in dom g
by A2, A3, XTUPLE_0:def 13; g . y = f . (x,y)
hence
g . y = f . (x,y)
by A2, A3; verum