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 g' being Function st
( (curry f) . x = g' & dom g' = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g' holds
g' . y = f . x,y ) ) by FUNCT_5:def 3;
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;
A3: ( [y,z] in dom f & [y,z] in [:{x},(proj2 (dom f)):] ) by A2, XBOOLE_0:def 4;
then y in {x} by ZFMISC_1:106;
hence [x,z] in dom f by A3, TARSKI:def 1; :: thesis: verum