let f, g be Function; :: thesis: for x, y, z being object st [x,y] in dom f & g = (curry f) . x & z in dom g holds
[x,z] in dom f
let x, y, z be object ; :: thesis: ( [x,y] in dom f & g = (curry f) . x & z in dom g implies [x,z] in dom f )
assume [x,y] in dom f ; :: thesis: ( not g = (curry f) . x or not z in dom g or [x,z] in dom f )
then x in proj1 (dom f) by XTUPLE_0:def 12;
then A1: ex g9 being Function st
( (curry f) . x = g9 & dom g9 = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g9 holds
g9 . y = f . (x,y) ) ) by FUNCT_5:def 1;
assume ( g = (curry f) . x & z in dom g ) ; :: thesis: [x,z] in dom f
then consider y being object such that
A2: [y,z] in (dom f) /\ [:{x},(proj2 (dom f)):] by A1, XTUPLE_0:def 13;
[y,z] in [:{x},(proj2 (dom f)):] by A2, XBOOLE_0:def 4;
then A3: y in {x} by ZFMISC_1:87;
[y,z] in dom f by A2, XBOOLE_0:def 4;
hence [x,z] in dom f by A3, TARSKI:def 1; :: thesis: verum