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