theorem LM4: :: LOPBAN13:8

for X being non trivial RealBanachSpace
for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,X))
for w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st v = w holds
( ( v is invertible implies w is invertible ) & ( w is invertible implies v is invertible ) & ( w is invertible implies v " = w " ) )