let E, G, F be RealNormSpace; :: thesis:
let Z be Subset of [:E,F:]; :: thesis:
let f be PartFunc of [:E,F:],G; :: thesis:
let a be Point of E; :: thesis:
let b be Point of F; :: thesis:
let c be Point of G; :: thesis:
let z be Point of [:E,F:]; :: thesis:
let A be Subset of E; :: thesis:
let B be Subset of F; :: thesis:
let g be PartFunc of E,F; :: thesis:
assume A1: ( Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible ) ; :: thesis:
then b in rng g by FUNCT_1:def 3;
then consider r2 being Real such that
A3: ( 0 < r2 & Ball (b,r2) c= B ) by A1, NDIFF_8:20;
consider r3 being Real such that
A4: ( 0 < r3 & ( for x1 being Point of E st x1 in dom g & ||.(x1 - a).|| < r3 holds
||.((g /. x1) - (g /. a)).|| < r2 ) ) by A1, A3, NFCONT_1:7;
consider r4 being Real such that
A5: ( 0 < r4 & Ball (a,r4) c= A ) by A1, NDIFF_8:20;
set r1 = min (r3,r4);
A6: ( 0 < min (r3,r4) & min (r3,r4) <= r3 & min (r3,r4) <= r4 ) by A4, A5, XXREAL_0:17, XXREAL_0:21;
set g1 = g | (Ball (a,(min (r3,r4))));
B6: Ball (a,(min (r3,r4))) c= Ball (a,r4) by A6, NDIFF_8:15;
then A7: Ball (a,(min (r3,r4))) c= A by A5, XBOOLE_1:1;
A8: dom (g | (Ball (a,(min (r3,r4))))) = Ball (a,(min (r3,r4))) by A1, A5, B6, RELAT_1:62, XBOOLE_1:1;

let y be object ; :: thesis:
assume A9: y in rng (g | (Ball (a,(min (r3,r4))))) ; :: thesis:
then consider x being object such that
A10: ( x in dom (g | (Ball (a,(min (r3,r4))))) & y = (g | (Ball (a,(min (r3,r4))))) . x ) by FUNCT_1:def 3;
reconsider xp = x as Point of E by A10;
A12: x in Ball (a,r4) by A6, A8, A10, NDIFF_8:15, TARSKI:def 3;
reconsider yp = y as Point of F by A9;
xp in { xx where xx is Point of E : ||.(xx - a).|| < min (r3,r4) } by A8, A10, NDIFF_8:17;
then ex z being Point of E st
( z = xp & ||.(z - a).|| < min (r3,r4) ) ;
then ||.(xp - a).|| < r3 by A6, XXREAL_0:2;
then A13: ||.((g /. xp) - (g /. a)).|| < r2 by A1, A4, A5, A12;
A14: y = g . xp by A8, A10, FUNCT_1:49
.= g /. xp by A1, A5, A12, PARTFUN1:def 6 ;
b = g /. a by A1, PARTFUN1:def 6;
then yp in { z where z is Point of F : ||.(z - b).|| < r2 } by A13, A14;
hence y in Ball (b,r2) by NDIFF_8:17; :: thesis:

end;

A17: a in Ball (a,(min (r3,r4))) by A6, NDIFF_8:13;
A26: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in dom (g | (Ball (a,(min (r3,r4))))) & ||.(x1 - a).|| < s holds
||.(((g | (Ball (a,(min (r3,r4))))) /. x1) - ((g | (Ball (a,(min (r3,r4))))) /. a)).|| < r ) )

proof

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider s being Real such that
A20: ( 0 < s & ( for x1 being Point of E st x1 in dom g & ||.(x1 - a).|| < s holds
||.((g /. x1) - (g /. a)).|| < r ) ) by A1, NFCONT_1:7;
take s ; :: thesis:
thus 0 < s by A20; :: thesis:
let x1 be Point of E; :: thesis:
assume A21: ( x1 in dom (g | (Ball (a,(min (r3,r4))))) & ||.(x1 - a).|| < s ) ; :: thesis:
then A25: g /. x1 = g . x1 by A1, A7, A8, PARTFUN1:def 6
.= (g | (Ball (a,(min (r3,r4))))) . x1 by A8, A21, FUNCT_1:49
.= (g | (Ball (a,(min (r3,r4))))) /. x1 by A21, PARTFUN1:def 6 ;
g /. a = g . a by A1, PARTFUN1:def 6
.= (g | (Ball (a,(min (r3,r4))))) . a by A6, FUNCT_1:49, NDIFF_8:13
.= (g | (Ball (a,(min (r3,r4))))) /. a by A6, A8, NDIFF_8:13, PARTFUN1:def 6 ;
hence ||.(((g | (Ball (a,(min (r3,r4))))) /. x1) - ((g | (Ball (a,(min (r3,r4))))) /. a)).|| < r by A1, A7, A8, A20, A21, A25; :: thesis:

end;

A28: for x being Point of E st x in Ball (a,(min (r3,r4))) holds
f . (x,((g | (Ball (a,(min (r3,r4))))) . x)) = c

proof

let x be Point of E; :: thesis:
assume A29: x in Ball (a,(min (r3,r4))) ; :: thesis:
then f . (x,(g . x)) = c by A1, A7;
hence f . (x,((g | (Ball (a,(min (r3,r4))))) . x)) = c by A29, FUNCT_1:49; :: thesis:

end;

b in Ball (b,r2) by A3, NDIFF_8:13;
then A31: [a,b] in [:(Ball (a,(min (r3,r4)))),(Ball (b,r2)):] by A17, ZFMISC_1:87;
A32: [:(Ball (a,(min (r3,r4)))),(Ball (b,r2)):] c= [:A,B:] by A3, A7, ZFMISC_1:96;
reconsider Q = (partdiff`2 (f,z)) " as Lipschitzian LinearOperator of G,F by A1, LOPBAN_1:def 9;
reconsider P = partdiff`1 (f,z) as Lipschitzian LinearOperator of E,G by LOPBAN_1:def 9;
( Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < min (r3,r4) & 0 < r2 & dom (g | (Ball (a,(min (r3,r4))))) = Ball (a,(min (r3,r4))) & rng (g | (Ball (a,(min (r3,r4))))) c= Ball (b,r2) & (g | (Ball (a,(min (r3,r4))))) . a = b & g | (Ball (a,(min (r3,r4)))) is_continuous_in a & ( for x being Point of E st x in Ball (a,(min (r3,r4))) holds
f . (x,((g | (Ball (a,(min (r3,r4))))) . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) ) by A1, A3, A6, A8, B8, A26, A28, A31, A32, FUNCT_1:49, NDIFF_8:13, NFCONT_1:7, TARSKI:def 3;
then A33: ( g | (Ball (a,(min (r3,r4)))) is_differentiable_in a & diff ((g | (Ball (a,(min (r3,r4))))),a) = - (Q * P) ) by Th5;
then consider N being Neighbourhood of a such that
A34: ( N c= dom (g | (Ball (a,(min (r3,r4))))) & ex R being RestFunc of E,F st
for x being Point of E st x in N holds
((g | (Ball (a,(min (r3,r4))))) /. x) - ((g | (Ball (a,(min (r3,r4))))) /. a) = ((diff ((g | (Ball (a,(min (r3,r4))))),a)) . (x - a)) + (R /. (x - a)) ) by NDIFF_1:def 7;
consider R being RestFunc of E,F such that
A35: for x being Point of E st x in N holds
((g | (Ball (a,(min (r3,r4))))) /. x) - ((g | (Ball (a,(min (r3,r4))))) /. a) = ((diff ((g | (Ball (a,(min (r3,r4))))),a)) . (x - a)) + (R /. (x - a)) by A34;
A37: N c= A by A7, A8, A34, XBOOLE_1:1;
A38: N c= dom g by A1, A7, A8, A34, XBOOLE_1:1;
A39: for x being Point of E st x in N holds
(g /. x) - (g /. a) = ((diff ((g | (Ball (a,(min (r3,r4))))),a)) . (x - a)) + (R /. (x - a))

proof

let x be Point of E; :: thesis:
assume A40: x in N ; :: thesis:
then A46: g /. x = g . x by A1, A37, PARTFUN1:def 6
.= (g | (Ball (a,(min (r3,r4))))) . x by A8, A34, A40, FUNCT_1:49
.= (g | (Ball (a,(min (r3,r4))))) /. x by A34, A40, PARTFUN1:def 6 ;
g /. a = g . a by A1, PARTFUN1:def 6
.= (g | (Ball (a,(min (r3,r4))))) . a by A6, FUNCT_1:49, NDIFF_8:13
.= (g | (Ball (a,(min (r3,r4))))) /. a by A6, A8, NDIFF_8:13, PARTFUN1:def 6 ;
hence (g /. x) - (g /. a) = ((diff ((g | (Ball (a,(min (r3,r4))))),a)) . (x - a)) + (R /. (x - a)) by A35, A40, A46; :: thesis:

end;

hence g is_differentiable_in a by A1, A7, A8, A34, NDIFF_1:def 6, XBOOLE_1:1; :: thesis:
then A48: diff (g,a) = diff ((g | (Ball (a,(min (r3,r4))))),a) by A38, A39, NDIFF_1:def 7;
Q = Inv (partdiff`2 (f,z)) by A1, LOPBAN13:def 2;
then modetrans ((Inv (partdiff`2 (f,z))),G,F) = Q by LOPBAN_1:def 11;
then A51: (Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z)) = Q * P by LOPBAN_1:def 11;
then Q * P is Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
hence diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) by A33, A48, A51, LOPBAN13:31; :: thesis: