let X, Y be non trivial RealBanachSpace; :: thesis:
let I be PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)); :: thesis:
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:
set S = R_NormSpace_of_BoundedLinearOperators (X,Y);
set T = InvertibleOperators (X,Y);
for x0 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for r being Real st x0 in InvertibleOperators (X,Y) & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st x1 in InvertibleOperators (X,Y) & ||.(x1 - x0).|| < s holds
||.((I /. x1) - (I /. x0)).|| < r ) )

let x0 be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis:
let r be Real; :: thesis:
assume A2: ( x0 in InvertibleOperators (X,Y) & 0 < r ) ; :: thesis:
then ex u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( x0 = u & u is invertible ) ;
then consider s being Real such that
A4: ( 0 < s & ( for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - x0).|| < s holds
||.((Inv v) - (Inv x0)).|| < r ) ) by A2, LMTh3;
take s ; :: thesis:
thus 0 < s by A4; :: thesis:
let x1 be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis:
assume A5: ( x1 in InvertibleOperators (X,Y) & ||.(x1 - x0).|| < s ) ; :: thesis:
A7: I /. x0 = I . x0 by A1, A2, PARTFUN1:def 6
.= Inv x0 by A1, A2 ;
I /. x1 = I . x1 by A1, A5, PARTFUN1:def 6
.= Inv x1 by A1, A5 ;
hence ||.((I /. x1) - (I /. x0)).|| < r by A4, A5, A7; :: thesis:

end;

hence I is_continuous_on InvertibleOperators (X,Y) by A1, NFCONT_1:19; :: thesis: