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 ) ) ) )
assume A1: ( 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 A2: ( dom g = proj2 ((dom (~ f)) /\ [:{x},(proj2 (dom (~ f))):]) & dom g c= proj2 (dom (~ f)) & rng g c= rng (~ f) & rng (~ f) c= rng f & ( for y being set st y in dom g holds
g . y = (~ f) . x,y ) ) by Th38, FUNCT_4:42;
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 dom (~ f) & [y,z] in [:{x},(proj1 (dom f)):] ) by A5, XBOOLE_0:def 4;
then ( [z,y] in dom f & [z,y] in [:(proj1 (dom f)),{x}:] ) by FUNCT_4:43, ZFMISC_1:107;
then [z,y] in (dom f) /\ [:(proj1 (dom f)),{x}:] by 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
A6: [z,y] in (dom f) /\ [:(proj1 (dom f)),{x}:] by RELAT_1:def 4;
( [z,y] in dom f & [z,y] in [:(proj1 (dom f)),{x}:] ) by A6, XBOOLE_0:def 4;
then ( [y,z] in dom (~ f) & [y,z] in [:{x},(proj1 (dom f)):] ) by FUNCT_4:43, ZFMISC_1:107;
then [y,z] in (dom (~ f)) /\ [:{x},(proj1 (dom f)):] by XBOOLE_0:def 4;
hence z in dom g by A3, RELAT_1:def 5; :: thesis: verum

end;

thus ( dom g c= proj1 (dom f) & rng g c= rng f ) by A2, 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 A7: y in dom g ; :: thesis: ( g . y = f . y,x & [y,x] in dom f )
then consider z being set such that
A8: [y,z] in (dom f) /\ [:(proj1 (dom f)),{x}:] by A4, RELAT_1:def 4;
( [y,z] in dom f & [y,z] in [:(proj1 (dom f)),{x}:] ) by A8, XBOOLE_0:def 4;
then ( [z,y] in dom (~ f) & z = x ) by FUNCT_4:43, ZFMISC_1:129;
then ( (~ f) . x,y = f . y,x & [y,x] in dom f ) by FUNCT_4:43, FUNCT_4:44;
hence ( g . y = f . y,x & [y,x] in dom f ) by A1, A7, Th38; :: thesis: verum