let X, Y be non trivial RealBanachSpace; :: thesis: for I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) st dom I = InvertibleOperators (X,Y) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) holds
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
( I is_differentiable_in u & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )
let I be PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)); :: thesis: ( dom I = InvertibleOperators (X,Y) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) implies for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
( I is_differentiable_in u & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) ) )
assume A1: ( dom I = InvertibleOperators (X,Y) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) ) ; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
( I is_differentiable_in u & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )
set S = R_NormSpace_of_BoundedLinearOperators (X,Y);
set W = R_NormSpace_of_BoundedLinearOperators (Y,X);
set N = InvertibleOperators (X,Y);
set P = InvertibleOperators (Y,X);
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( u in InvertibleOperators (X,Y) implies ( I is_differentiable_in u & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) ) )
assume A2: u in InvertibleOperators (X,Y) ; :: thesis: ( I is_differentiable_in u & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )
deffunc H₁( Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))) -> Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) = - (((Inv u) * $1) * (Inv u));
consider L being Function of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)), the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) such that
A3: for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds L . x = H₁(x) from FUNCT_2:sch 4();
A6: for s, t being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds L . (s + t) = (L . s) + (L . t)

proof

let s, t be Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: L . (s + t) = (L . s) + (L . t)
thus L . (s + t) = - (((Inv u) * (s + t)) * (Inv u)) by A3
.= - ((((Inv u) * s) + ((Inv u) * t)) * (Inv u)) by LOPBAN13:19
.= - ((((Inv u) * s) * (Inv u)) + (((Inv u) * t) * (Inv u))) by LOPBAN13:20
.= (- (((Inv u) * s) * (Inv u))) - (((Inv u) * t) * (Inv u)) by RLVECT_1:31
.= (L . s) + (- (((Inv u) * t) * (Inv u))) by A3
.= (L . s) + (L . t) by A3 ; :: thesis: verum

end;

for s being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for r being Real holds L . (r * s) = r * (L . s)

proof

let s be Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for r being Real holds L . (r * s) = r * (L . s)
let r be Real; :: thesis: L . (r * s) = r * (L . s)
thus L . (r * s) = - (((Inv u) * (r * s)) * (Inv u)) by A3
.= - (((r * (Inv u)) * s) * (Inv u)) by LOPBAN13:28
.= - ((r * ((Inv u) * s)) * (Inv u)) by LOPBAN13:28
.= - (r * (((Inv u) * s) * (Inv u))) by LOPBAN13:28
.= r * (- (((Inv u) * s) * (Inv u))) by RLVECT_1:25
.= r * (L . s) by A3 ; :: thesis: verum

end;

then reconsider L = L as LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) by A6, LOPBAN_1:def 5, VECTSP_1:def 20;

now :: thesis: for x being VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ||.(L . x).|| <= (||.(Inv u).|| * ||.(Inv u).||) * ||.x.||

let x be VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ||.(L . x).|| <= (||.(Inv u).|| * ||.(Inv u).||) * ||.x.||
L . x = - (((Inv u) * x) * (Inv u)) by A3;
then A8: ||.(L . x).|| = ||.(((Inv u) * x) * (Inv u)).|| by NORMSP_1:2;
A9: ||.(((Inv u) * x) * (Inv u)).|| <= ||.((Inv u) * x).|| * ||.(Inv u).|| by LOPBAN13:18;
||.((Inv u) * x).|| * ||.(Inv u).|| <= (||.(Inv u).|| * ||.x.||) * ||.(Inv u).|| by LOPBAN13:18, XREAL_1:64;
hence ||.(L . x).|| <= (||.(Inv u).|| * ||.(Inv u).||) * ||.x.|| by A8, A9, XXREAL_0:2; :: thesis: verum

end;

then reconsider L = L as Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) by LOPBAN_1:def 8;
deffunc H₂( Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))) -> Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) = ((Inv (u + $1)) - (Inv u)) - (L . $1);
consider R being Function of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)), the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) such that
A11: for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds R . x = H₂(x) from FUNCT_2:sch 4();
A12: dom R = the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by FUNCT_2:def 1;
A13: for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds R . x = ((Inv (u + x)) - (Inv u)) - (- (((Inv u) * x) * (Inv u)))

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: R . x = ((Inv (u + x)) - (Inv u)) - (- (((Inv u) * x) * (Inv u)))
thus R . x = ((Inv (u + x)) - (Inv u)) - (L . x) by A11
.= ((Inv (u + x)) - (Inv u)) - (- (((Inv u) * x) * (Inv u))) by A3 ; :: thesis: verum

end;

reconsider L0 = L as Point of (R_NormSpace_of_BoundedLinearOperators ((R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)))) by LOPBAN_1:def 9;
for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st z <> 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) )

proof

let r0 be Real; :: thesis: ( r0 > 0 implies ex d being Real st
( d > 0 & ( for z being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st z <> 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r0 ) ) )
assume A15: r0 > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for z being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st z <> 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r0 ) )
set r = r0 / 2;
A16: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A15, XREAL_1:215, XREAL_1:216;
ex v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( u = v & v is invertible ) by A2;
then consider K, s being Real such that
A17: ( 0 <= K & 0 < s & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds
( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= K * (||.du.|| * ||.du.||) ) ) ) by LMTh3;
set s1 = (r0 / 2) / (K + 1);
A18: K + 0 < K + 1 by XREAL_1:8;
A20: 0 < (r0 / 2) / (K + 1) by A16, A17, XREAL_1:139;
set s2 = min (((r0 / 2) / (K + 1)),1);
A21: ( 0 < min (((r0 / 2) / (K + 1)),1) & min (((r0 / 2) / (K + 1)),1) <= (r0 / 2) / (K + 1) & min (((r0 / 2) / (K + 1)),1) <= 1 ) by A20, XXREAL_0:15, XXREAL_0:17;
set d = min (s,(min (((r0 / 2) / (K + 1)),1)));
A22: ( 0 < min (s,(min (((r0 / 2) / (K + 1)),1))) & min (s,(min (((r0 / 2) / (K + 1)),1))) <= s & min (s,(min (((r0 / 2) / (K + 1)),1))) <= min (((r0 / 2) / (K + 1)),1) ) by A17, A21, XXREAL_0:15, XXREAL_0:17;
then A23: ( min (s,(min (((r0 / 2) / (K + 1)),1))) <= s & min (s,(min (((r0 / 2) / (K + 1)),1))) <= (r0 / 2) / (K + 1) & min (s,(min (((r0 / 2) / (K + 1)),1))) <= 1 ) by A21, XXREAL_0:2;
take min (s,(min (((r0 / 2) / (K + 1)),1))) ; :: thesis: ( min (s,(min (((r0 / 2) / (K + 1)),1))) > 0 & ( for z being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st z <> 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) & ||.z.|| < min (s,(min (((r0 / 2) / (K + 1)),1))) holds
(||.z.|| ") * ||.(R /. z).|| < r0 ) )
thus min (s,(min (((r0 / 2) / (K + 1)),1))) > 0 by A17, A21, XXREAL_0:15; :: thesis: for z being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st z <> 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) & ||.z.|| < min (s,(min (((r0 / 2) / (K + 1)),1))) holds
(||.z.|| ") * ||.(R /. z).|| < r0
let z be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( z <> 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) & ||.z.|| < min (s,(min (((r0 / 2) / (K + 1)),1))) implies (||.z.|| ") * ||.(R /. z).|| < r0 )
assume A24: ( z <> 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) & ||.z.|| < min (s,(min (((r0 / 2) / (K + 1)),1))) ) ; :: thesis: (||.z.|| ") * ||.(R /. z).|| < r0
then A25: ||.z.|| < s by A22, XXREAL_0:2;
||.(R /. z).|| = ||.(((Inv (u + z)) - (Inv u)) - (- (((Inv u) * z) * (Inv u)))).|| by A13;
then ||.(R /. z).|| <= K * (||.z.|| * ||.z.||) by A17, A25;
then ||.(R /. z).|| / ||.z.|| <= ((K * ||.z.||) * ||.z.||) / ||.z.|| by XREAL_1:72;
then A27: ||.(R /. z).|| / ||.z.|| <= K * ||.z.|| by A24, NORMSP_0:def 5, XCMPLX_1:89;
||.z.|| <= (r0 / 2) / (K + 1) by A23, A24, XXREAL_0:2;
then A28: K * ||.z.|| <= K * ((r0 / 2) / (K + 1)) by A17, XREAL_1:64;
K / (K + 1) <= 1 by A17, A18, XREAL_1:183;
then (r0 / 2) * (K / (K + 1)) <= 1 * (r0 / 2) by A15, XREAL_1:64;
then K * ||.z.|| <= r0 / 2 by A28, XXREAL_0:2;
then ||.(R /. z).|| / ||.z.|| <= r0 / 2 by A27, XXREAL_0:2;
hence (||.z.|| ") * ||.(R /. z).|| < r0 by A16, XXREAL_0:2; :: thesis: verum

end;

then reconsider R0 = R as RestFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) by NDIFF_1:23;
ex g being Real st
( 0 < g & { y where y is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : ||.(y - u).|| < g } c= InvertibleOperators (X,Y) ) by A2, NDIFF_1:3;
then A29: InvertibleOperators (X,Y) is Neighbourhood of u by NFCONT_1:def 1;
A30: for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st v in InvertibleOperators (X,Y) holds
(I /. v) - (I /. u) = (L0 . (v - u)) + (R0 /. (v - u))

proof

let v be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( v in InvertibleOperators (X,Y) implies (I /. v) - (I /. u) = (L0 . (v - u)) + (R0 /. (v - u)) )
assume A31: v in InvertibleOperators (X,Y) ; :: thesis: (I /. v) - (I /. u) = (L0 . (v - u)) + (R0 /. (v - u))
then A32: I /. v = I . v by A1, PARTFUN1:def 6
.= Inv v by A1, A31 ;
I /. u = I . u by A1, A2, PARTFUN1:def 6
.= Inv u by A1, A2 ;
hence (I /. v) - (I /. u) = (Inv (u + (v - u))) - (Inv u) by A32, RLVECT_4:1
.= (L0 . (v - u)) + (((Inv (u + (v - u))) - (Inv u)) - (L . (v - u))) by RLVECT_4:1
.= (L0 . (v - u)) + (((Inv (u + (v - u))) - (Inv u)) - (- (((Inv u) * (v - u)) * (Inv u)))) by A3
.= (L0 . (v - u)) + (R . (v - u)) by A13
.= (L0 . (v - u)) + (R0 /. (v - u)) by A12, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence A34: I is_differentiable_in u by A1, A29, NDIFF_1:def 6; :: thesis: for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (diff (I,u)) . du = - (((Inv u) * du) * (Inv u))
let du be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: (diff (I,u)) . du = - (((Inv u) * du) * (Inv u))
thus (diff (I,u)) . du = L0 . du by A1, A29, A30, A34, NDIFF_1:def 7
.= - (((Inv u) * du) * (Inv u)) by A3 ; :: thesis: verum