let X, Y be non trivial RealBanachSpace; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
( 0 < ||.u.|| & 0 < ||.(Inv u).|| )
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( u is invertible implies ( 0 < ||.u.|| & 0 < ||.(Inv u).|| ) )
assume A1: u is invertible ; :: thesis: ( 0 < ||.u.|| & 0 < ||.(Inv u).|| )
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
reconsider Lu = u 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;
A8: (BoundedLinearOperatorsNorm (X,X)) . (LInvu * Lu) <= ((BoundedLinearOperatorsNorm (Y,X)) . LInvu) * ((BoundedLinearOperatorsNorm (X,Y)) . Lu) by LOPBAN_2:2;
LInvu = u " by A1, Def1;
then (BoundedLinearOperatorsNorm (X,X)) . (LInvu * Lu) = ||.(1. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| by A1, FUNCT_2:29
.= 1 by LOPBAN_2:def 10 ;
then ( ||.(Inv u).|| <> 0 & ||.u.|| <> 0 ) by A8;
hence ( 0 < ||.u.|| & 0 < ||.(Inv u).|| ) ; :: thesis: verum