let X, Y be non trivial RealBanachSpace; :: thesis: for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible & ||.(v - u).|| < 1 / ||.(Inv u).|| holds
( v is invertible & ||.(Inv v).|| <= 1 / ((1 / ||.(Inv u).||) - ||.(v - u).||) & ex w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) st
( w = (Inv u) * (v - u) & s = w & I = id X & ||.s.|| < 1 & (- w) GeoSeq is norm_summable & I + s is invertible & ||.(Inv (I + s)).|| <= 1 / (1 - ||.s.||) & Inv (I + s) = Sum ((- w) GeoSeq) & Inv v = (Inv (I + s)) * (Inv u) ) )
let u, v be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( u is invertible & ||.(v - u).|| < 1 / ||.(Inv u).|| implies ( v is invertible & ||.(Inv v).|| <= 1 / ((1 / ||.(Inv u).||) - ||.(v - u).||) & ex w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) st
( w = (Inv u) * (v - u) & s = w & I = id X & ||.s.|| < 1 & (- w) GeoSeq is norm_summable & I + s is invertible & ||.(Inv (I + s)).|| <= 1 / (1 - ||.s.||) & Inv (I + s) = Sum ((- w) GeoSeq) & Inv v = (Inv (I + s)) * (Inv u) ) ) )
assume A1: ( u is invertible & ||.(v - u).|| < 1 / ||.(Inv u).|| ) ; :: thesis: ( v is invertible & ||.(Inv v).|| <= 1 / ((1 / ||.(Inv u).||) - ||.(v - u).||) & ex w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) st
( w = (Inv u) * (v - u) & s = w & I = id X & ||.s.|| < 1 & (- w) GeoSeq is norm_summable & I + s is invertible & ||.(Inv (I + s)).|| <= 1 / (1 - ||.s.||) & Inv (I + s) = Sum ((- w) GeoSeq) & Inv v = (Inv (I + s)) * (Inv u) ) )
set vu = v - u;
v = u + (v - u) by RLVECT_4:1;
hence ( v is invertible & ||.(Inv v).|| <= 1 / ((1 / ||.(Inv u).||) - ||.(v - u).||) & ex w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) st
( w = (Inv u) * (v - u) & s = w & I = id X & ||.s.|| < 1 & (- w) GeoSeq is norm_summable & I + s is invertible & ||.(Inv (I + s)).|| <= 1 / (1 - ||.s.||) & Inv (I + s) = Sum ((- w) GeoSeq) & Inv v = (Inv (I + s)) * (Inv u) ) ) by A1, Th2; :: thesis: verum