let x be object ; :: thesis: for f, g being Function st x in dom (curry' f) & g = (curry' f) . x holds
( dom g = proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (y,x) & [y,x] in dom f ) ) )
let f, g be Function; :: thesis: ( x in dom (curry' f) & g = (curry' f) . x implies ( dom g = proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (y,x) & [y,x] in dom f ) ) ) )
A1: rng (~ f) c= rng f by FUNCT_4:41;
assume A2: ( x in dom (curry' f) & g = (curry' f) . x ) ; :: thesis: ( dom g = proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (y,x) & [y,x] in dom f ) ) )
then dom g = proj2 ((dom (~ f)) /\ [:{x},(proj2 (dom (~ f))):]) by Th24;
then A3: dom g = proj2 ((dom (~ f)) /\ [:{x},(proj1 (dom f)):]) by Th11;
thus A4: dom g c= proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) :: according to XBOOLE_0:def 10 :: thesis: ( proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) c= dom g & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (y,x) & [y,x] in dom f ) ) )

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom g or z in proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) )
assume z in dom g ; :: thesis: z in proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:])
then consider y being object such that
A5: [y,z] in (dom (~ f)) /\ [:{x},(proj1 (dom f)):] by A3, XTUPLE_0:def 13;
[y,z] in [:{x},(proj1 (dom f)):] by A5, XBOOLE_0:def 4;
then A6: [z,y] in [:(proj1 (dom f)),{x}:] by ZFMISC_1:88;
[y,z] in dom (~ f) by A5, XBOOLE_0:def 4;
then [z,y] in dom f by FUNCT_4:42;
then [z,y] in (dom f) /\ [:(proj1 (dom f)),{x}:] by A6, XBOOLE_0:def 4;
hence z in proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) by XTUPLE_0:def 12; :: thesis: verum

end;

thus proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) c= dom g :: thesis: ( dom g c= proj1 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (y,x) & [y,x] in dom f ) ) )

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) or z in dom g )
assume z in proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) ; :: thesis: z in dom g
then consider y being object such that
A7: [z,y] in (dom f) /\ [:(proj1 (dom f)),{x}:] by XTUPLE_0:def 12;
[z,y] in [:(proj1 (dom f)),{x}:] by A7, XBOOLE_0:def 4;
then A8: [y,z] in [:{x},(proj1 (dom f)):] by ZFMISC_1:88;
[z,y] in dom f by A7, XBOOLE_0:def 4;
then [y,z] in dom (~ f) by FUNCT_4:42;
then [y,z] in (dom (~ f)) /\ [:{x},(proj1 (dom f)):] by A8, XBOOLE_0:def 4;
hence z in dom g by A3, XTUPLE_0:def 13; :: thesis: verum

end;

( dom g c= proj2 (dom (~ f)) & rng g c= rng (~ f) ) by A2, Th24;
hence ( dom g c= proj1 (dom f) & rng g c= rng f ) by A1, Th11; :: thesis: for y being object st y in dom g holds
( g . y = f . (y,x) & [y,x] in dom f )
let y be object ; :: thesis: ( y in dom g implies ( g . y = f . (y,x) & [y,x] in dom f ) )
assume A9: y in dom g ; :: thesis: ( g . y = f . (y,x) & [y,x] in dom f )
then consider z being object such that
A10: [y,z] in (dom f) /\ [:(proj1 (dom f)),{x}:] by A4, XTUPLE_0:def 12;
[y,z] in [:(proj1 (dom f)),{x}:] by A10, XBOOLE_0:def 4;
then A11: z = x by ZFMISC_1:106;
[y,z] in dom f by A10, XBOOLE_0:def 4;
then [z,y] in dom (~ f) by FUNCT_4:42;
then (~ f) . (x,y) = f . (y,x) by A11, FUNCT_4:43;
hence ( g . y = f . (y,x) & [y,x] in dom f ) by A2, A9, A10, A11, Th24, XBOOLE_0:def 4; :: thesis: verum