let x be object ; :: 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 object 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 object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f ) ) ) )
assume that
A1: x in dom (curry f) and
A2: 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 object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f ) ) )
dom (curry f) = proj1 (dom f) by Def1;
then consider h being Function such that
A3: (curry f) . x = h and
A4: dom h = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) and
A5: for y being object st y in dom h holds
h . y = f . (x,y) by A1, Def1;
thus dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) by A2, A3, A4; :: thesis: ( dom g c= proj2 (dom f) & rng g c= rng f & ( for y being object 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 A2, A3, A4, XTUPLE_0:9; :: thesis: ( rng g c= rng f & ( for y being object 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 object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f )

proof

let y be object ; :: 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 object such that
A6: z in dom g and
A7: y = g . z by FUNCT_1:def 3;
consider t being object such that
A8: [t,z] in (dom f) /\ [:{x},(proj2 (dom f)):] by A2, A3, A4, A6, XTUPLE_0:def 13;
( [t,z] in dom f & [t,z] in [:{x},(proj2 (dom f)):] ) by A8, XBOOLE_0:def 4;
then A9: [x,z] in dom f by ZFMISC_1:105;
h . z = f . (x,z) by A2, A3, A5, A6;
hence y in rng f by A2, A3, A7, A9, FUNCT_1:def 3; :: thesis: verum

end;

let y be object ; :: thesis: ( y in dom g implies ( g . y = f . (x,y) & [x,y] in dom f ) )
assume A10: y in dom g ; :: thesis: ( g . y = f . (x,y) & [x,y] in dom f )
then consider t being object such that
A11: [t,y] in (dom f) /\ [:{x},(proj2 (dom f)):] by A2, A3, A4, XTUPLE_0:def 13;
( [t,y] in dom f & [t,y] in [:{x},(proj2 (dom f)):] ) by A11, XBOOLE_0:def 4;
hence ( g . y = f . (x,y) & [x,y] in dom f ) by A2, A3, A5, A10, ZFMISC_1:105; :: thesis: verum