let f, g be Function; :: thesis: 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 ; :: thesis: ( [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 ; :: thesis: ( 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; :: thesis: g . y = f . (x,y)
hence g . y = f . (x,y) by A2, A3; :: thesis: verum