let X, Y be non trivial RealBanachSpace; :: thesis:
let u, v be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis:
assume that
A1: u is invertible and
A2: ||.v.|| < 1 / ||.(Inv u).|| ; :: thesis:
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
1. (R_Normed_Algebra_of_BoundedLinearOperators X) = id X ;
then reconsider I = id X as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
reconsider Is = I as Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ;
A6: u is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
A7: v is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
reconsider udv = (Inv u) * v as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
reconsider udv2 = udv as Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ;
reconsider Lu = u, Lv = v as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
reconsider LInvu = Inv u as Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 9;
A14: ( modetrans (LInvu,Y,X) = LInvu & modetrans (Lv,X,Y) = Lv ) by LOPBAN_1:29;
then A15: ||.udv.|| <= ||.(Inv u).|| * ||.v.|| by LOPBAN_2:2;
LInvu = u " by A1, Def1;
then A17: (BoundedLinearOperatorsNorm (X,X)) . (LInvu * Lu) = ||.(1. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| by A1, FUNCT_2:29
.= 1 by LOPBAN_2:def 10 ;
A18: ||.(Inv u).|| <> 0

assume ||.(Inv u).|| = 0 ; :: thesis:
then 1 <= 0 * ((BoundedLinearOperatorsNorm (X,Y)) . u) by A17, LOPBAN_2:2;
hence contradiction ; :: thesis:

end;

then ||.(Inv u).|| * ||.v.|| < ||.(Inv u).|| * (1 / ||.(Inv u).||) by A2, XREAL_1:68;
then A20: ||.(Inv u).|| * ||.v.|| < 1 by A18, XCMPLX_1:106;
then A21: ||.udv.|| < 1 by A15, XXREAL_0:2;
then A22: ( I + udv is invertible & ||.(Inv (I + udv)).|| <= 1 / (1 - ||.udv.||) & ex w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st
( w = udv & (- w) GeoSeq is norm_summable & Inv (I + udv) = Sum ((- w) GeoSeq) ) ) by Th1;
A23: u + v is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
then A24: modetrans ((u + v),X,Y) = u + v by LOPBAN_1:29;
A25: I + udv is Lipschitzian LinearOperator of X,X by LOPBAN_1:def 9;
then A26: modetrans ((I + udv),X,X) = I + udv by LOPBAN_1:29;
A27: modetrans (u,X,Y) = u by A6, LOPBAN_1:29;
A28: for x being Element of the carrier of X holds (u + v) . x = (u * (I + udv)) . x

let x be Element of the carrier of X; :: thesis:
A33: (u * (I + udv)) . x = (modetrans (u,X,Y)) . ((modetrans ((I + udv),X,X)) . x) by FUNCT_2:15
.= u . ((I + udv) . x) by A25, A27, LOPBAN_1:29 ;
A35: (I + udv) . x = ((id X) . x) + (udv . x) by LOPBAN_1:35
.= x + (udv . x) ;
Lu is additive ;
then A37: Lu . ((I + udv) . x) = (Lu . x) + (Lu . (udv . x)) by A35;
A39: Inv u is Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 9;
A40: modetrans (v,X,Y) = v by A7, LOPBAN_1:29;
u . (udv . x) = u . ((modetrans ((Inv u),Y,X)) . ((modetrans (v,X,Y)) . x)) by FUNCT_2:15
.= u . ((Inv u) . (v . x)) by A39, A40, LOPBAN_1:29
.= u . ((u ") . (v . x)) by A1, Def1
.= v . x by A1, FUNCT_1:35 ;
hence (u + v) . x = (u * (I + udv)) . x by A33, A37, LOPBAN_1:35; :: thesis:

end;

then A43: u + v is one-to-one by A1, A22, A23, A26, A27, FUNCT_2:def 7;
A44: modetrans (u,X,Y) is onto by A1, A6, LOPBAN_1:29;
modetrans ((I + udv),X,X) is onto by A22, A25, LOPBAN_1:29;
then (modetrans (u,X,Y)) * (modetrans ((I + udv),X,X)) is onto by A44, FUNCT_2:27;
then A46: rng (u + v) = the carrier of Y by A23, A28, FUNCT_2:def 7;
set Iuv = (Inv (I + udv)) * (Inv u);
(Inv (I + udv)) * (Inv u) is Lipschitzian LinearOperator of Y,X by LOPBAN_2:2;
then A48: modetrans (((Inv (I + udv)) * (Inv u)),Y,X) = (Inv (I + udv)) * (Inv u) by LOPBAN_1:29;
Inv u is Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 9;
then A49: modetrans ((Inv u),Y,X) = Inv u by LOPBAN_1:29;
B49: Inv (I + udv) is Lipschitzian LinearOperator of X,X by LOPBAN_1:def 9;
then A50: modetrans ((Inv (I + udv)),X,X) = Inv (I + udv) by LOPBAN_1:29;
A51: modetrans (((I + udv) "),X,X) = modetrans ((Inv (I + udv)),X,X) by A21, Def1, Th1
.= Inv (I + udv) by B49, LOPBAN_1:29
.= (I + udv) " by A21, Def1, Th1 ;
modetrans ((Inv u),Y,X) = u " by A1, A49, Def1;
then A53: (Inv u) * u = (u ") * u by A6, LOPBAN_1:29
.= id X by A1, FUNCT229 ;
(Inv u) * u is Lipschitzian LinearOperator of X,X by LOPBAN_2:2;
then modetrans (((Inv u) * u),X,X) = id X by A53, LOPBAN_1:29;
then A55: ((Inv u) * u) * (I + udv) = (id X) * (I + udv) by A25, LOPBAN_1:29
.= I + udv by A25, FUNCT_2:17 ;
A56: (modetrans (((Inv (I + udv)) * (Inv u)),Y,X)) * (modetrans ((u + v),X,Y)) = ((Inv (I + udv)) * (Inv u)) * (u + v)
.= (Inv (I + udv)) * ((Inv u) * (u + v)) by RELAT136
.= (Inv (I + udv)) * ((Inv u) * (u * (I + udv))) by A23, A28, FUNCT_2:def 7
.= (Inv (I + udv)) * (I + udv) by A55, RELAT136
.= (modetrans (((I + udv) "),X,X)) * (modetrans ((I + udv),X,X)) by A21, Def1, Th1
.= ((I + udv) ") * (I + udv) by A25, A51, LOPBAN_1:29
.= id X by A22, FUNCT229 ;
then A57: (modetrans ((u + v),X,Y)) " = modetrans (((Inv (I + udv)) * (Inv u)),Y,X) by A24, A43, A46, FUNCT_2:30;
thus A58: u + v is invertible by A24, A43, A46, A48, A56, FUNCT_2:30; :: thesis:
reconsider Iuvp = (Inv (I + udv)) * (Inv u) as Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) ;
A59: (BoundedLinearOperatorsNorm (Y,X)) . ((Inv (I + udv)) * (Inv u)) <= ((BoundedLinearOperatorsNorm (X,X)) . (modetrans ((Inv (I + udv)),X,X))) * ((BoundedLinearOperatorsNorm (Y,X)) . (modetrans ((Inv u),Y,X))) by LOPBAN_2:2;
((BoundedLinearOperatorsNorm (X,X)) . (Inv (I + udv))) * ((BoundedLinearOperatorsNorm (Y,X)) . (Inv u)) <= (1 / (1 - ||.udv.||)) * ||.(Inv u).|| by A22, XREAL_1:64;
then A64: ||.Iuvp.|| <= (1 / (1 - ||.udv.||)) * ||.(Inv u).|| by A49, A50, A59, XXREAL_0:2;
A65: 1 - (||.(Inv u).|| * ||.v.||) <= 1 - ||.udv.|| by A14, LOPBAN_2:2, XREAL_1:10;
0 < 1 - (||.(Inv u).|| * ||.v.||) by A20, XREAL_1:50;
then 1 / (1 - ||.udv.||) <= 1 / (1 - (||.(Inv u).|| * ||.v.||)) by A65, XREAL_1:118;
then (1 / (1 - ||.udv.||)) * ||.(Inv u).|| <= (1 / (1 - (||.(Inv u).|| * ||.v.||))) * ||.(Inv u).|| by XREAL_1:64;
then A67: (1 / (1 - ||.udv.||)) * ||.(Inv u).|| <= ||.(Inv u).|| / (1 - (||.(Inv u).|| * ||.v.||)) by XCMPLX_1:99;
(1 - (||.(Inv u).|| * ||.v.||)) / ||.(Inv u).|| = (1 / ||.(Inv u).||) - ((||.(Inv u).|| * ||.v.||) / ||.(Inv u).||) by XCMPLX_1:120
.= (1 / ||.(Inv u).||) - ||.v.|| by A18, XCMPLX_1:89 ;
then 1 / ((1 / ||.(Inv u).||) - ||.v.||) = ||.(Inv u).|| / (1 - (||.(Inv u).|| * ||.v.||)) by XCMPLX_1:57;
then ||.Iuvp.|| <= 1 / ((1 / ||.(Inv u).||) - ||.v.||) by A64, A67, XXREAL_0:2;
hence ||.(Inv (u + v)).|| <= 1 / ((1 / ||.(Inv u).||) - ||.v.||) by A24, A48, A57, A58, Def1; :: thesis:
consider w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) such that
A70: ( w = udv & (- w) GeoSeq is norm_summable & Inv (I + udv) = Sum ((- w) GeoSeq) ) by A21, Th1;
reconsider S = Sum ((- w) GeoSeq) as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
take w ; :: thesis:
take udv ; :: thesis:
take I ; :: thesis:
thus ( w = (Inv u) * v & udv = w & I = id X & ||.udv.|| < 1 & (- w) GeoSeq is norm_summable & I + udv is invertible & ||.(Inv (I + udv)).|| <= 1 / (1 - ||.udv.||) & Inv (I + udv) = Sum ((- w) GeoSeq) ) by A21, A70, Th1; :: thesis:
thus Inv (u + v) = (Inv (I + udv)) * (Inv u) by A24, A48, A57, A58, Def1; :: thesis: