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
I is_continuous_on InvertibleOperators (X,Y)
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 I is_continuous_on InvertibleOperators (X,Y) )
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: I is_continuous_on InvertibleOperators (X,Y)
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 ) )

proof

let x0 be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: 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 r be Real; :: thesis: ( x0 in InvertibleOperators (X,Y) & 0 < r implies 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 ) ) )
assume A2: ( x0 in InvertibleOperators (X,Y) & 0 < r ) ; :: thesis: 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 ) )
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: ( 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 ) )
thus 0 < s by A4; :: thesis: 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 x1 be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( x1 in InvertibleOperators (X,Y) & ||.(x1 - x0).|| < s implies ||.((I /. x1) - (I /. x0)).|| < r )
assume A5: ( x1 in InvertibleOperators (X,Y) & ||.(x1 - x0).|| < s ) ; :: thesis: ||.((I /. x1) - (I /. x0)).|| < r
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: verum

end;

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