let E, G, F be RealNormSpace; :: thesis: for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:]
for r1, r2 being Real
for g being PartFunc of E,F
for P being Lipschitzian LinearOperator of E,G
for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )
let Z be Subset of [:E,F:]; :: thesis: for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:]
for r1, r2 being Real
for g being PartFunc of E,F
for P being Lipschitzian LinearOperator of E,G
for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )
let f be PartFunc of [:E,F:],G; :: thesis: for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:]
for r1, r2 being Real
for g being PartFunc of E,F
for P being Lipschitzian LinearOperator of E,G
for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )
let a be Point of E; :: thesis: for b being Point of F
for c being Point of G
for z being Point of [:E,F:]
for r1, r2 being Real
for g being PartFunc of E,F
for P being Lipschitzian LinearOperator of E,G
for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )
let b be Point of F; :: thesis: for c being Point of G
for z being Point of [:E,F:]
for r1, r2 being Real
for g being PartFunc of E,F
for P being Lipschitzian LinearOperator of E,G
for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )
let c be Point of G; :: thesis: for z being Point of [:E,F:]
for r1, r2 being Real
for g being PartFunc of E,F
for P being Lipschitzian LinearOperator of E,G
for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )
let z be Point of [:E,F:]; :: thesis: for r1, r2 being Real
for g being PartFunc of E,F
for P being Lipschitzian LinearOperator of E,G
for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )
let r1, r2 be Real; :: thesis: for g being PartFunc of E,F
for P being Lipschitzian LinearOperator of E,G
for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )
let g be PartFunc of E,F; :: thesis: for P being Lipschitzian LinearOperator of E,G
for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )
let P be Lipschitzian LinearOperator of E,G; :: thesis: for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )
let Q be Lipschitzian LinearOperator of G,F; :: thesis: ( Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) implies ( g is_differentiable_in a & diff (g,a) = - (Q * P) ) )
assume A1: ( Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) ) ; :: thesis: ( g is_differentiable_in a & diff (g,a) = - (Q * P) )
then A5: g /. a = b by NDIFF_8:13, PARTFUN1:def 6;
reconsider S = partdiff`2 (f,z) as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
A8: Q * P is Lipschitzian LinearOperator of E,F by LOPBAN_2:2;
then reconsider L = Q * P as Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) by LOPBAN_1:def 9;
A9: (- 1) * L is Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
reconsider NL = (- 1) * L as PartFunc of E,F by LOPBAN_1:def 9;
A10: dom NL = the carrier of E by A9, FUNCT_2:def 1
.= dom (Q * P) by FUNCT_2:def 1 ;

A11: now :: thesis: for x being VECTOR of E st x in dom NL holds
NL /. x = (- 1) * ((Q * P) /. x)

let x be VECTOR of E; :: thesis: ( x in dom NL implies NL /. x = (- 1) * ((Q * P) /. x) )
assume x in dom NL ; :: thesis: NL /. x = (- 1) * ((Q * P) /. x)
hence NL /. x = ((- 1) * L) . x by PARTFUN1:def 6
.= (- 1) * ((Q * P) /. x) by LOPBAN_1:36 ;
:: thesis: verum

end;

A15: - L = (- 1) * L by RLVECT_1:16
.= (- 1) (#) (Q * P) by A10, A11, VFUNCT_1:def 4
.= - (Q * P) by VFUNCT_1:23 ;
consider N0 being Neighbourhood of z such that
A16: ( N0 c= dom f & ex R being RestFunc of [:E,F:],G st
for w being Point of [:E,F:] st w in N0 holds
(f /. w) - (f /. z) = ((diff (f,z)) . (w - z)) + (R /. (w - z)) ) by A1, NDIFF_1:def 7;
consider R being RestFunc of [:E,F:],G such that
A17: for w being Point of [:E,F:] st w in N0 holds
(f /. w) - (f /. z) = ((diff (f,z)) . (w - z)) + (R /. (w - z)) by A16;
consider r0 being Real such that
A20: ( 0 < r0 & { y where y is Point of [:E,F:] : ||.(y - z).|| < r0 } c= N0 ) by NFCONT_1:def 1;
A21: { y where y is Point of [:E,F:] : ||.(y - z).|| < r0 } = Ball (z,r0) by NDIFF_8:17;
consider r3 being Real such that
A22: ( 0 < r3 & r3 < r0 & [:(Ball (a,r3)),(Ball (b,r3)):] c= Ball (z,r0) ) by A1, A20, NDIFF_8:22;
A23: [:(Ball (a,r3)),(Ball (b,r3)):] c= N0 by A20, A21, A22, XBOOLE_1:1;
reconsider r4 = min (r1,r3) as Real ;
A24: 0 < r4 by A1, A22, XXREAL_0:15;
( r4 <= r1 & r4 <= r3 ) by XXREAL_0:17;
then A26: ( Ball (a,r4) c= Ball (a,r1) & Ball (a,r4) c= Ball (a,r3) ) by NDIFF_8:15;
consider r5 being Real such that
A27: ( 0 < r5 & ( for x1 being Point of E st x1 in dom g & ||.(x1 - a).|| < r5 holds
||.((g /. x1) - (g /. a)).|| < r3 ) ) by A1, A22, NFCONT_1:7;
reconsider r6 = min (r4,r5) as Real ;
A28: 0 < r6 by A24, A27, XXREAL_0:15;
( r6 <= r4 & r6 <= r5 ) by XXREAL_0:17;
then A30: ( Ball (a,r6) c= Ball (a,r4) & Ball (a,r6) c= Ball (a,r5) ) by NDIFF_8:15;
reconsider N = Ball (a,r6) as Neighbourhood of a by A28, NDIFF_8:19;
deffunc H₁( Point of E) -> Element of the carrier of F = - (Q . (R /. [$1,((g /. (a + $1)) - (g /. a))]));
consider R1 being Function of the carrier of E, the carrier of F such that
A31: for p being Point of E holds R1 . p = H₁(p) from FUNCT_2:sch 4();
A33: N c= dom g by A1, A26, A30, XBOOLE_1:1;
A34: for x being Point of E st x in N holds
(g /. x) - (g /. a) = ((- L) . (x - a)) + (R1 /. (x - a))

proof

let x be Point of E; :: thesis: ( x in N implies (g /. x) - (g /. a) = ((- L) . (x - a)) + (R1 /. (x - a)) )
assume x in N ; :: thesis: (g /. x) - (g /. a) = ((- L) . (x - a)) + (R1 /. (x - a))
then A36: ( x in Ball (a,r4) & x in Ball (a,r5) ) by A30;
then x in { y where y is Point of E : ||.(y - a).|| < r5 } by NDIFF_8:17;
then ex q being Element of E st
( x = q & ||.(q - a).|| < r5 ) ;
then ||.((g /. x) - (g /. a)).|| < r3 by A1, A26, A27, A36;
then g /. x in { y where y is Point of F : ||.(y - b).|| < r3 } by A5;
then A39: g /. x in Ball (b,r3) by NDIFF_8:17;
A41: f . (x,(g . x)) = c by A1, A26, A36;
A42: [x,(g /. x)] in [:(Ball (a,r3)),(Ball (b,r3)):] by A26, A36, A39, ZFMISC_1:87;
then A45: [x,(g /. x)] in N0 by A23;
reconsider w = [x,(g /. x)] as Point of [:E,F:] ;
A47: (f /. w) - (f /. z) = ((diff (f,z)) . (w - z)) + (R /. (w - z)) by A17, A23, A42;
A48: f /. z = c by A1, PARTFUN1:def 6;
A50: f /. w = f . [x,(g /. x)] by A16, A45, PARTFUN1:def 6
.= c by A1, A26, A36, A41, PARTFUN1:def 6 ;
- z = [(- a),(- b)] by A1, PRVECT_3:18;
then A52: w - z = [(x - a),((g /. x) - b)] by PRVECT_3:18
.= [(x - a),((g /. x) - (g /. a))] by A1, NDIFF_8:13, PARTFUN1:def 6 ;
then (diff (f,z)) . (w - z) = ((partdiff`1 (f,z)) . (x - a)) + ((partdiff`2 (f,z)) . ((g /. x) - (g /. a))) by A1, Th4;
then 0. G = ((P . (x - a)) + (S . ((g /. x) - (g /. a)))) + (R /. (w - z)) by A1, A47, A48, A50, RLVECT_1:15;
then 0. F = Q . (((P . (x - a)) + (S . ((g /. x) - (g /. a)))) + (R /. (w - z))) by LOPBAN_7:3;
then 0. F = (Q . ((P . (x - a)) + (S . ((g /. x) - (g /. a))))) + (Q . (R /. (w - z))) by VECTSP_1:def 20
.= ((Q . (P . (x - a))) + (Q . (S . ((g /. x) - (g /. a))))) + (Q . (R /. (w - z))) by VECTSP_1:def 20
.= (((Q * P) . (x - a)) + (Q . (S . ((g /. x) - (g /. a))))) + (Q . (R /. (w - z))) by FUNCT_2:15
.= (((Q * P) . (x - a)) + ((g /. x) - (g /. a))) + (Q . (R /. (w - z))) by A1, FUNCT_2:26 ;
then (0. F) - (Q . (R /. (w - z))) = ((Q * P) . (x - a)) + ((g /. x) - (g /. a)) by RLVECT_4:1;
then A53: (- (Q . (R /. (w - z)))) - ((Q * P) . (x - a)) = (((g /. x) - (g /. a)) + ((Q * P) . (x - a))) - ((Q * P) . (x - a)) by RLVECT_1:14
.= (g /. x) - (g /. a) by RLVECT_4:1 ;
A54: dom (- (Q * P)) = dom (Q * P) by VFUNCT_1:def 5
.= the carrier of E by FUNCT_2:def 1 ;
A55: - ((Q * P) . (x - a)) = - ((Q * P) /. (x - a))
.= (- (Q * P)) /. (x - a) by A54, VFUNCT_1:def 5
.= (- L) . (x - a) by A15, A54, PARTFUN1:def 6 ;
R1 /. (x - a) = - (Q . (R /. [(x - a),((g /. ((x - a) + a)) - (g /. a))])) by A31
.= - (Q . (R /. (w - z))) by A52, RLVECT_4:1 ;
hence (g /. x) - (g /. a) = ((- L) . (x - a)) + (R1 /. (x - a)) by A53, A55; :: thesis: verum

end;

defpred S₁[ Point of E, object ] means $2 = [$1,((g /. (a + $1)) - (g /. a))];
A59: for dx being Element of the carrier of E ex dy being Element of the carrier of [:E,F:] st S₁[dx,dy] ;
consider V being Function of the carrier of E, the carrier of [:E,F:] such that
A60: for dx being Element of the carrier of E holds S₁[dx,V . dx] from FUNCT_2:sch 3(A59);
A62: R is total by NDIFF_1:def 5;
reconsider Q1 = Q as Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) by LOPBAN_1:def 9;
set BLQ = ||.Q1.||;
0 * (||.Q1.|| + 1) < 2 * (||.Q1.|| + 1) by XREAL_1:68;
then consider dr being Real such that
A65: ( dr > 0 & ( for dz being Point of [:E,F:] st dz <> 0. [:E,F:] & ||.dz.|| < dr holds
(||.dz.|| ") * ||.(R /. dz).|| < 1 / (2 * (||.Q1.|| + 1)) ) ) by A62, NDIFF_1:23;
consider dr1 being Real such that
A66: ( 0 < dr1 & dr1 < dr & [:(Ball (a,dr1)),(Ball ((g /. a),dr1)):] c= Ball (z,dr) ) by A1, A5, A65, NDIFF_8:22;
consider dr2 being Real such that
A67: ( 0 < dr2 & ( for x1 being Point of E st x1 in dom g & ||.(x1 - a).|| < dr2 holds
||.((g /. x1) - (g /. a)).|| < dr1 ) ) by A1, A66, NFCONT_1:7;
reconsider dr3 = min (dr1,dr2) as Real ;
A69: ( dr3 <= dr1 & dr3 <= dr2 ) by XXREAL_0:17;
reconsider dr4 = min (dr3,r1) as Real ;
0 < dr3 by A66, A67, XXREAL_0:15;
then A71: 0 < dr4 by A1, XXREAL_0:15;
A72: ( dr4 <= dr3 & dr4 <= r1 ) by XXREAL_0:17;
A74: for dx being Point of E st dx <> 0. E & ||.dx.|| < dr4 holds
||.(R /. (V . dx)).|| <= (1 / (2 * (||.Q1.|| + 1))) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)

proof

let dx be Point of E; :: thesis: ( dx <> 0. E & ||.dx.|| < dr4 implies ||.(R /. (V . dx)).|| <= (1 / (2 * (||.Q1.|| + 1))) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) )
set x1 = a + dx;
assume A75: ( dx <> 0. E & ||.dx.|| < dr4 ) ; :: thesis: ||.(R /. (V . dx)).|| <= (1 / (2 * (||.Q1.|| + 1))) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)
then A76: ||.((a + dx) - a).|| < dr4 by RLVECT_4:1;
then ||.((a + dx) - a).|| < dr3 by A72, XXREAL_0:2;
then A78: ( ||.((a + dx) - a).|| < dr1 & ||.((a + dx) - a).|| < dr2 ) by A69, XXREAL_0:2;
then ||.(a - (a + dx)).|| < dr1 by NORMSP_1:7;
then A79: a + dx in Ball (a,dr1) ;
||.(a - (a + dx)).|| < dr4 by A76, NORMSP_1:7;
then ( ||.(a - (a + dx)).|| < r1 & ||.(a - (a + dx)).|| < dr3 ) by A72, XXREAL_0:2;
then a + dx in Ball (a,r1) ;
then ||.((g /. (a + dx)) - (g /. a)).|| < dr1 by A1, A67, A78;
then ||.((g /. a) - (g /. (a + dx))).|| < dr1 by NORMSP_1:7;
then g /. (a + dx) in Ball ((g /. a),dr1) ;
then [(a + dx),(g /. (a + dx))] in [:(Ball (a,dr1)),(Ball ((g /. a),dr1)):] by A79, ZFMISC_1:87;
then [(a + dx),(g /. (a + dx))] in Ball (z,dr) by A66;
then consider w being Point of [:E,F:] such that
A84: ( w = [(a + dx),(g /. (a + dx))] & ||.(z - w).|| < dr ) ;
- z = [(- a),(- (g /. a))] by A1, A5, PRVECT_3:18;
then A86: w - z = [((a + dx) - a),((g /. (a + dx)) - (g /. a))] by A84, PRVECT_3:18;
A87: ||.(w - z).|| < dr by A84, NORMSP_1:7;
(a + dx) - a = dx by RLVECT_4:1;
then A88: w - z <> 0. [:E,F:] by A75, A86, XTUPLE_0:1;
then ||.(w - z).|| <> 0 by NORMSP_0:def 5;
then ((||.(w - z).|| ") * ||.(R /. (w - z)).||) * ||.(w - z).|| < (1 / (2 * (||.Q1.|| + 1))) * ||.(w - z).|| by A65, A87, A88, XREAL_1:68;
then (||.(w - z).|| ") * (||.(R /. (w - z)).|| * ||.(w - z).||) < (1 / (2 * (||.Q1.|| + 1))) * ||.(w - z).|| ;
then A91: ||.(R /. (w - z)).|| < (1 / (2 * (||.Q1.|| + 1))) * ||.(w - z).|| by A88, NORMSP_0:def 5, XCMPLX_1:203;
A92: V . dx = [dx,((g /. (a + dx)) - (g /. a))] by A60
.= [((a + dx) - a),((g /. (a + dx)) - (g /. a))] by RLVECT_4:1 ;
then A94: (1 / (2 * (||.Q1.|| + 1))) * ||.(V . dx).|| <= (1 / (2 * (||.Q1.|| + 1))) * (||.((a + dx) - a).|| + ||.((g /. (a + dx)) - (g /. a)).||) by LM0, XREAL_1:64;
( g /. (a + dx) = g /. (a + dx) & (a + dx) - a = dx ) by RLVECT_4:1;
hence ||.(R /. (V . dx)).|| <= (1 / (2 * (||.Q1.|| + 1))) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) by A86, A91, A92, A94, XXREAL_0:2; :: thesis: verum

end;

A95: for dx being Point of E st dx <> 0. E & ||.dx.|| < dr4 holds
||.(R1 /. dx).|| <= (1 / 2) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)

proof

let dx be Point of E; :: thesis: ( dx <> 0. E & ||.dx.|| < dr4 implies ||.(R1 /. dx).|| <= (1 / 2) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) )
assume ( dx <> 0. E & ||.dx.|| < dr4 ) ; :: thesis: ||.(R1 /. dx).|| <= (1 / 2) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)
then A97: ||.(R /. (V . dx)).|| <= (1 / (2 * (||.Q1.|| + 1))) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) by A74;
A98: ||.(Q . (R /. (V . dx))).|| <= ||.Q1.|| * ||.(R /. (V . dx)).|| by LOPBAN_1:32;
A99: ||.Q1.|| * ||.(R /. (V . dx)).|| <= ||.Q1.|| * ((1 / (2 * (||.Q1.|| + 1))) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||)) by A97, XREAL_1:64;
A101: ||.Q1.|| * (1 / (2 * (||.Q1.|| + 1))) = (1 * ||.Q1.||) / (2 * (||.Q1.|| + 1))
.= (1 / 2) * (||.Q1.|| / (||.Q1.|| + 1)) by XCMPLX_1:103 ;
||.Q1.|| + 0 <= ||.Q1.|| + 1 by XREAL_1:7;
then ||.Q1.|| / (||.Q1.|| + 1) <= 1 by XREAL_1:183;
then (1 / 2) * (||.Q1.|| / (||.Q1.|| + 1)) <= (1 / 2) * 1 by XREAL_1:64;
then (||.Q1.|| * (1 / (2 * (||.Q1.|| + 1)))) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) <= (1 / 2) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) by A101, XREAL_1:64;
then ||.Q1.|| * ||.(R /. (V . dx)).|| <= (1 / 2) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) by A99, XXREAL_0:2;
then A102: ||.(Q . (R /. (V . dx))).|| <= (1 / 2) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) by A98, XXREAL_0:2;
- (Q . (R /. (V . dx))) = - (Q . (R /. [dx,((g /. (a + dx)) - (g /. a))])) by A60
.= R1 /. dx by A31 ;
hence ||.(R1 /. dx).|| <= (1 / 2) * (||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).||) by A102, NORMSP_1:2; :: thesis: verum

end;

set LQ = ||.L.||;
reconsider dr5 = min (r6,dr4) as Real ;
A104: 0 < dr5 by A28, A71, XXREAL_0:15;
A105: ( dr5 <= r6 & dr5 <= dr4 ) by XXREAL_0:17;
A107: for dx being Point of E st dx <> 0. E & ||.dx.|| < dr5 holds
||.((g /. (a + dx)) - (g /. a)).|| <= ((2 * ||.L.||) + 1) * ||.dx.||

proof

let dx be Point of E; :: thesis: ( dx <> 0. E & ||.dx.|| < dr5 implies ||.((g /. (a + dx)) - (g /. a)).|| <= ((2 * ||.L.||) + 1) * ||.dx.|| )
assume A108: ( dx <> 0. E & ||.dx.|| < dr5 ) ; :: thesis: ||.((g /. (a + dx)) - (g /. a)).|| <= ((2 * ||.L.||) + 1) * ||.dx.||
then A109: ||.dx.|| < dr4 by A105, XXREAL_0:2;
A111: ||.dx.|| < r6 by A105, A108, XXREAL_0:2;
set x1 = a + dx;
A112: (a + dx) - a = dx by RLVECT_4:1;
then ||.(a - (a + dx)).|| < r6 by A111, NORMSP_1:7;
then a + dx in N ;
then (g /. (a + dx)) - (g /. a) = ((- L) . ((a + dx) - a)) + (R1 /. ((a + dx) - a)) by A34;
then A114: ||.((g /. (a + dx)) - (g /. a)).|| <= ||.((- L) . ((a + dx) - a)).|| + ||.(R1 /. ((a + dx) - a)).|| by NORMSP_1:def 1;
(- L) . ((a + dx) - a) = ((- 1) * L) . ((a + dx) - a) by RLVECT_1:16
.= (- 1) * ((Q * P) . ((a + dx) - a)) by LOPBAN_1:36
.= - ((Q * P) . ((a + dx) - a)) by RLVECT_1:16 ;
then ||.((- L) . ((a + dx) - a)).|| = ||.((Q * P) . ((a + dx) - a)).|| by NORMSP_1:2;
then A115: ||.((- L) . ((a + dx) - a)).|| <= ||.L.|| * ||.((a + dx) - a).|| by A8, LOPBAN_1:32;
||.(R1 /. ((a + dx) - a)).|| <= (1 / 2) * (||.((a + dx) - a).|| + ||.((g /. (a + dx)) - (g /. a)).||) by A95, A108, A109, A112;
then ||.((- L) . ((a + dx) - a)).|| + ||.(R1 /. ((a + dx) - a)).|| <= (||.L.|| * ||.((a + dx) - a).||) + (((1 / 2) * ||.((a + dx) - a).||) + ((1 / 2) * ||.((g /. (a + dx)) - (g /. a)).||)) by A115, XREAL_1:7;
then ||.((g /. (a + dx)) - (g /. a)).|| <= ((||.L.|| * ||.((a + dx) - a).||) + ((1 / 2) * ||.((a + dx) - a).||)) + ((1 / 2) * ||.((g /. (a + dx)) - (g /. a)).||) by A114, XXREAL_0:2;
then ||.((g /. (a + dx)) - (g /. a)).|| - ((1 / 2) * ||.((g /. (a + dx)) - (g /. a)).||) <= (((||.L.|| * ||.((a + dx) - a).||) + ((1 / 2) * ||.((a + dx) - a).||)) + ((1 / 2) * ||.((g /. (a + dx)) - (g /. a)).||)) - ((1 / 2) * ||.((g /. (a + dx)) - (g /. a)).||) by XREAL_1:9;
then 2 * ((1 / 2) * ||.((g /. (a + dx)) - (g /. a)).||) <= 2 * ((||.L.|| * ||.((a + dx) - a).||) + ((1 / 2) * ||.((a + dx) - a).||)) by XREAL_1:64;
hence ||.((g /. (a + dx)) - (g /. a)).|| <= ((2 * ||.L.||) + 1) * ||.dx.|| by A112; :: thesis: verum

end;

for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for dx being Point of E st dx <> 0. E & ||.dx.|| < d holds
(||.dx.|| ") * ||.(R1 /. dx).|| < r ) )

proof

let r be Real; :: thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for dx being Point of E st dx <> 0. E & ||.dx.|| < d holds
(||.dx.|| ") * ||.(R1 /. dx).|| < r ) ) )
assume A117: r > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for dx being Point of E st dx <> 0. E & ||.dx.|| < d holds
(||.dx.|| ") * ||.(R1 /. dx).|| < r ) )
A120: 0 < (||.Q1.|| + 1) * ((2 * ||.L.||) + 2) by XREAL_1:129;
then 0 < r / ((||.Q1.|| + 1) * ((2 * ||.L.||) + 2)) by A117, XREAL_1:139;
then consider d1 being Real such that
A122: ( d1 > 0 & ( for dz being Point of [:E,F:] st dz <> 0. [:E,F:] & ||.dz.|| < d1 holds
(||.dz.|| ") * ||.(R /. dz).|| < r / ((||.Q1.|| + 1) * ((2 * ||.L.||) + 2)) ) ) by A62, NDIFF_1:23;
consider r3 being Real such that
A123: ( 0 < r3 & r3 < d1 & [:(Ball (a,r3)),(Ball (b,r3)):] c= Ball (z,d1) ) by A1, A122, NDIFF_8:22;
reconsider r4 = min (r1,r3) as Real ;
A124: 0 < r4 by A1, A123, XXREAL_0:15;
A125: ( r4 <= r1 & r4 <= r3 ) by XXREAL_0:17;
consider r5 being Real such that
A127: ( 0 < r5 & ( for x1 being Point of E st x1 in dom g & ||.(x1 - a).|| < r5 holds
||.((g /. x1) - (g /. a)).|| < r3 ) ) by A1, A123, NFCONT_1:7;
reconsider r6 = min (r4,r5) as Real ;
A128: 0 < r6 by A124, A127, XXREAL_0:15;
A129: ( r6 <= r4 & r6 <= r5 ) by XXREAL_0:17;
reconsider d = min (r6,dr5) as Real ;
A132: ( d <= r6 & d <= dr5 ) by XXREAL_0:17;
take d ; :: thesis: ( d > 0 & ( for dx being Point of E st dx <> 0. E & ||.dx.|| < d holds
(||.dx.|| ") * ||.(R1 /. dx).|| < r ) )
thus 0 < d by A104, A128, XXREAL_0:15; :: thesis: for dx being Point of E st dx <> 0. E & ||.dx.|| < d holds
(||.dx.|| ") * ||.(R1 /. dx).|| < r
let dx be Point of E; :: thesis: ( dx <> 0. E & ||.dx.|| < d implies (||.dx.|| ") * ||.(R1 /. dx).|| < r )
assume A133: ( dx <> 0. E & ||.dx.|| < d ) ; :: thesis: (||.dx.|| ") * ||.(R1 /. dx).|| < r
set x1 = a + dx;
reconsider dz = [dx,((g /. (a + dx)) - (g /. a))] as Point of [:E,F:] ;
A134: dz <> 0. [:E,F:] by A133, XTUPLE_0:1;
A137: ||.dx.|| < dr5 by A132, A133, XXREAL_0:2;
A138: ||.dx.|| < r6 by A132, A133, XXREAL_0:2;
then A139: ||.dx.|| < r5 by A129, XXREAL_0:2;
||.dx.|| < r4 by A129, A138, XXREAL_0:2;
then A140: ( ||.dx.|| < r1 & ||.dx.|| < r3 ) by A125, XXREAL_0:2;
then ||.((a + dx) - a).|| < r1 by RLVECT_4:1;
then ||.(a - (a + dx)).|| < r1 by NORMSP_1:7;
then A141: a + dx in dom g by A1;
||.((a + dx) - a).|| < r5 by A139, RLVECT_4:1;
then ||.((g /. (a + dx)) - (g /. a)).|| < r3 by A127, A141;
then ||.((g /. a) - (g /. (a + dx))).|| < r3 by NORMSP_1:7;
then A142: g /. (a + dx) in Ball (b,r3) by A5;
||.((a + dx) - a).|| < r3 by A140, RLVECT_4:1;
then ||.(a - (a + dx)).|| < r3 by NORMSP_1:7;
then a + dx in Ball (a,r3) ;
then [(a + dx),(g /. (a + dx))] in [:(Ball (a,r3)),(Ball (b,r3)):] by A142, ZFMISC_1:87;
then [(a + dx),(g /. (a + dx))] in Ball (z,d1) by A123;
then consider w being Point of [:E,F:] such that
A145: ( w = [(a + dx),(g /. (a + dx))] & ||.(z - w).|| < d1 ) ;
- z = [(- a),(- (g /. a))] by A1, A5, PRVECT_3:18;
then w - z = [((a + dx) - a),((g /. (a + dx)) - (g /. a))] by A145, PRVECT_3:18
.= dz by RLVECT_4:1 ;
then A148: ||.dz.|| < d1 by A145, NORMSP_1:7;
R1 /. dx = - (Q . (R /. [dx,((g /. (a + dx)) - (g /. a))])) by A31;
then ||.(R1 /. dx).|| = ||.(Q . (R /. [dx,((g /. (a + dx)) - (g /. a))])).|| by NORMSP_1:2;
then A150: ||.(R1 /. dx).|| <= ||.Q1.|| * ||.(R /. [dx,((g /. (a + dx)) - (g /. a))]).|| by LOPBAN_1:32;
0 + ||.Q1.|| < ||.Q1.|| + 1 by XREAL_1:8;
then ||.Q1.|| * ||.(R /. [dx,((g /. (a + dx)) - (g /. a))]).|| <= (||.Q1.|| + 1) * ||.(R /. [dx,((g /. (a + dx)) - (g /. a))]).|| by XREAL_1:64;
then ||.(R1 /. dx).|| <= (||.Q1.|| + 1) * ||.(R /. [dx,((g /. (a + dx)) - (g /. a))]).|| by A150, XXREAL_0:2;
then (||.dx.|| ") * ||.(R1 /. dx).|| <= (||.dx.|| ") * ((||.Q1.|| + 1) * ||.(R /. [dx,((g /. (a + dx)) - (g /. a))]).||) by XREAL_1:64;
then (||.dx.|| ") * ||.(R1 /. dx).|| <= ((||.dx.|| ") * (||.Q1.|| + 1)) * ||.(R /. dz).|| ;
then A152: (||.dx.|| ") * ||.(R1 /. dx).|| <= ((||.dx.|| ") * (||.Q1.|| + 1)) * ((||.dz.|| ") * (||.(R /. dz).|| * ||.dz.||)) by A134, NORMSP_0:def 5, XCMPLX_1:203;
A153: ||.dz.|| <= ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).|| by LM0;
||.((g /. (a + dx)) - (g /. a)).|| <= ((2 * ||.L.||) + 1) * ||.dx.|| by A107, A133, A137;
then ||.dx.|| + ||.((g /. (a + dx)) - (g /. a)).|| <= ||.dx.|| + (((2 * ||.L.||) + 1) * ||.dx.||) by XREAL_1:7;
then ||.dz.|| <= ||.dx.|| + (((2 * ||.L.||) + 1) * ||.dx.||) by A153, XXREAL_0:2;
then (||.dx.|| ") * ||.dz.|| <= (||.dx.|| ") * (||.dx.|| + (((2 * ||.L.||) + 1) * ||.dx.||)) by XREAL_1:64;
then (||.dx.|| ") * ||.dz.|| <= ((||.dx.|| ") * (||.dx.|| * 1)) + ((||.dx.|| ") * (((2 * ||.L.||) + 1) * ||.dx.||)) ;
then (||.dx.|| ") * ||.dz.|| <= 1 + ((||.dx.|| ") * (((2 * ||.L.||) + 1) * ||.dx.||)) by A133, NORMSP_0:def 5, XCMPLX_1:203;
then (||.dx.|| ") * ||.dz.|| <= 1 + ((2 * ||.L.||) + 1) by A133, NORMSP_0:def 5, XCMPLX_1:203;
then ((||.Q1.|| + 1) * ((||.dz.|| ") * ||.(R /. dz).||)) * ((||.dx.|| ") * ||.dz.||) <= ((||.Q1.|| + 1) * ((||.dz.|| ") * ||.(R /. dz).||)) * ((2 * ||.L.||) + 2) by XREAL_1:64;
then A159: (||.dx.|| ") * ||.(R1 /. dx).|| <= ((||.Q1.|| + 1) * ((2 * ||.L.||) + 2)) * ((||.dz.|| ") * ||.(R /. dz).||) by A152, XXREAL_0:2;
((||.Q1.|| + 1) * ((2 * ||.L.||) + 2)) * ((||.dz.|| ") * ||.(R /. dz).||) < ((||.Q1.|| + 1) * ((2 * ||.L.||) + 2)) * (r / ((||.Q1.|| + 1) * ((2 * ||.L.||) + 2))) by A120, A122, A134, A148, XREAL_1:68;
then ((||.Q1.|| + 1) * ((2 * ||.L.||) + 2)) * ((||.dz.|| ") * ||.(R /. dz).||) < r by A120, XCMPLX_1:87;
hence (||.dx.|| ") * ||.(R1 /. dx).|| < r by A159, XXREAL_0:2; :: thesis: verum

end;

then A162: R1 is RestFunc of E,F by NDIFF_1:23;
hence g is_differentiable_in a by A1, A26, A30, A34, NDIFF_1:def 6, XBOOLE_1:1; :: thesis: diff (g,a) = - (Q * P)
hence diff (g,a) = - (Q * P) by A15, A33, A34, A162, NDIFF_1:def 7; :: thesis: verum