theorem Th63: :: NDIFF13:62

for E, F, G being RealNormSpace
for x being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for L being Point of (R_NormSpace_of_BoundedLinearOperators ((R_NormSpace_of_BoundedLinearOperators (F,E)),(R_NormSpace_of_BoundedLinearOperators (E,E)))) st x is invertible & ( for y being Point of (R_NormSpace_of_BoundedLinearOperators (F,E)) holds L . y = y * x ) holds
L is invertible