let X, Y be non trivial RealBanachSpace; :: thesis: for S being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st S = { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } holds
S is open
let S be Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( S = { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } implies S is open )
assume A1: S = { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } ; :: thesis: S is open
set P = R_NormSpace_of_BoundedLinearOperators (X,Y);
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in S holds
ex r being Real st
( r > 0 & Ball (u,r) c= S )

proof

let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( u in S implies ex r being Real st
( r > 0 & Ball (u,r) c= S ) )
assume u in S ; :: thesis: ex r being Real st
( r > 0 & Ball (u,r) c= S )
then A2: ex v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( u = v & v is invertible ) by A1;
then A3: 0 < ||.(Inv u).|| by LM50;
set r = 1 / ||.(Inv u).||;
take 1 / ||.(Inv u).|| ; :: thesis: ( 1 / ||.(Inv u).|| > 0 & Ball (u,(1 / ||.(Inv u).||)) c= S )
thus 0 < 1 / ||.(Inv u).|| by A3, XREAL_1:139; :: thesis: Ball (u,(1 / ||.(Inv u).||)) c= S

now :: thesis: for x being object st x in Ball (u,(1 / ||.(Inv u).||)) holds
x in S

let x be object ; :: thesis: ( x in Ball (u,(1 / ||.(Inv u).||)) implies x in S )
assume x in Ball (u,(1 / ||.(Inv u).||)) ; :: thesis: x in S
then x in { y where y is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : ||.(y - u).|| < 1 / ||.(Inv u).|| } by NDIFF_8:17;
then consider v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) such that
A4: ( x = v & ||.(v - u).|| < 1 / ||.(Inv u).|| ) ;
v = u + (v - u) by RLVECT_4:1;
then v is invertible by A2, A4, Th2;
hence x in S by A1, A4; :: thesis: verum

end;

hence Ball (u,(1 / ||.(Inv u).||)) c= S by TARSKI:def 3; :: thesis: verum

end;

hence S is open by NDIFF_8:20; :: thesis: verum