let x, y be set ; :: thesis: for f, g being Function st [x,y] in dom f & g = (curry f) . x holds
( y in dom g & g . y = f . x,y )
let f, g be Function; :: 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, RELAT_1:def 4;
then A3: ex h being Function st
( (curry f) . x = h & dom h = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom h holds
h . y = f . x,y ) ) by Def3;
y in proj2 (dom f) by A1, RELAT_1:def 5;
then [x,y] in [:{x},(proj2 (dom f)):] by ZFMISC_1:128;
then [x,y] in (dom f) /\ [:{x},(proj2 (dom f)):] by A1, XBOOLE_0:def 4;
hence y in dom g by A2, A3, RELAT_1:def 5; :: thesis: g . y = f . x,y
hence g . y = f . x,y by A2, A3; :: thesis: verum