let x be set ; :: thesis: for f, g being Function st x in dom (curry f) & g = (curry f) . x holds
( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds
( g . y = f . x,y & [x,y] in dom f ) ) )
let f, g be Function; :: thesis: ( x in dom (curry f) & g = (curry f) . x implies ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds
( g . y = f . x,y & [x,y] in dom f ) ) ) )
assume A1: ( x in dom (curry f) & g = (curry f) . x ) ; :: thesis: ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds
( g . y = f . x,y & [x,y] in dom f ) ) )
dom (curry f) = proj1 (dom f) by Def3;
then consider h being Function such that
A2: ( (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 A1, Def3;
thus dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) by A1, A2; :: thesis: ( dom g c= proj2 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds
( g . y = f . x,y & [x,y] in dom f ) ) )
(dom f) /\ [:{x},(proj2 (dom f)):] c= dom f by XBOOLE_1:17;
hence dom g c= proj2 (dom f) by A1, A2, Th5; :: thesis: ( rng g c= rng f & ( for y being set st y in dom g holds
( g . y = f . x,y & [x,y] in dom f ) ) )
thus rng g c= rng f :: thesis: for y being set st y in dom g holds
( g . y = f . x,y & [x,y] in dom f )

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in rng f )
assume y in rng g ; :: thesis: y in rng f
then consider z being set such that
A3: ( z in dom g & y = g . z ) by FUNCT_1:def 5;
consider t being set such that
A4: [t,z] in (dom f) /\ [:{x},(proj2 (dom f)):] by A1, A2, A3, RELAT_1:def 5;
( [t,z] in dom f & [t,z] in [:{x},(proj2 (dom f)):] ) by A4, XBOOLE_0:def 4;
then ( h . z = f . x,z & [x,z] in dom f ) by A1, A2, A3, ZFMISC_1:128;
hence y in rng f by A1, A2, A3, FUNCT_1:def 5; :: thesis: verum

end;

let y be set ; :: thesis: ( y in dom g implies ( g . y = f . x,y & [x,y] in dom f ) )
assume A5: y in dom g ; :: thesis: ( g . y = f . x,y & [x,y] in dom f )
then consider t being set such that
A6: [t,y] in (dom f) /\ [:{x},(proj2 (dom f)):] by A1, A2, RELAT_1:def 5;
( [t,y] in dom f & [t,y] in [:{x},(proj2 (dom f)):] ) by A6, XBOOLE_0:def 4;
hence ( g . y = f . x,y & [x,y] in dom f ) by A1, A2, A5, ZFMISC_1:128; :: thesis: verum