theorem Th66:
for
F,
G being non
trivial RealBanachSpace ex
I being
PartFunc of
(R_NormSpace_of_BoundedLinearOperators (F,G)),
(R_NormSpace_of_BoundedLinearOperators (G,F)) st
(
dom I = InvertibleOperators (
F,
G) &
rng I = InvertibleOperators (
G,
F) &
I is
one-to-one &
I is_continuous_on InvertibleOperators (
F,
G) & ex
J being
PartFunc of
(R_NormSpace_of_BoundedLinearOperators (G,F)),
(R_NormSpace_of_BoundedLinearOperators (F,G)) st
(
J = I " &
J is
one-to-one &
dom J = InvertibleOperators (
G,
F) &
rng J = InvertibleOperators (
F,
G) &
J is_continuous_on InvertibleOperators (
G,
F) ) & ( for
u being
Point of
(R_NormSpace_of_BoundedLinearOperators (F,G)) st
u in InvertibleOperators (
F,
G) holds
I . u = Inv u ) & ( for
n being
Nat holds
(
I is_differentiable_on n + 1,
InvertibleOperators (
F,
G) &
diff (
I,
(n + 1),
(InvertibleOperators (F,G)))
is_continuous_on InvertibleOperators (
F,
G) ) ) )