let x be set ; :: 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 set 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 set 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:42;
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 set 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 Th38;
then A3: dom g = proj2 ((dom (~ f)) /\ [:{x},(proj1 (dom f)):]) by Th20;
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 set st y in dom g holds
( g . y = f . (y,x) & [y,x] in dom f ) ) )

proof

let z be set ; :: 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 set such that
A5: [y,z] in (dom (~ f)) /\ [:{x},(proj1 (dom f)):] by A3, RELAT_1:def 5;
[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:107;
[y,z] in dom (~ f) by A5, XBOOLE_0:def 4;
then [z,y] in dom f by FUNCT_4:43;
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 RELAT_1:def 4; :: 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 set st y in dom g holds
( g . y = f . (y,x) & [y,x] in dom f ) ) )

proof

let z be set ; :: 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 set such that
A7: [z,y] in (dom f) /\ [:(proj1 (dom f)),{x}:] by RELAT_1:def 4;
[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:107;
[z,y] in dom f by A7, XBOOLE_0:def 4;
then [y,z] in dom (~ f) by FUNCT_4:43;
then [y,z] in (dom (~ f)) /\ [:{x},(proj1 (dom f)):] by A8, XBOOLE_0:def 4;
hence z in dom g by A3, RELAT_1:def 5; :: thesis: verum

end;

( dom g c= proj2 (dom (~ f)) & rng g c= rng (~ f) ) by A2, Th38;
hence ( dom g c= proj1 (dom f) & rng g c= rng f ) by A1, Th20, XBOOLE_1:1; :: thesis: for y being set st y in dom g holds
( g . y = f . (y,x) & [y,x] in dom f )
let y be set ; :: 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 set such that
A10: [y,z] in (dom f) /\ [:(proj1 (dom f)),{x}:] by A4, RELAT_1:def 4;
[y,z] in [:(proj1 (dom f)),{x}:] by A10, XBOOLE_0:def 4;
then A11: z = x by ZFMISC_1:129;
[y,z] in dom f by A10, XBOOLE_0:def 4;
then [z,y] in dom (~ f) by FUNCT_4:43;
then (~ f) . (x,y) = f . (y,x) by A11, FUNCT_4:44;
hence ( g . y = f . (y,x) & [y,x] in dom f ) by A2, A9, A10, A11, Th38, XBOOLE_0:def 4; :: thesis: verum