theorem FUNCT229: :: LOPBAN13:11

for X, Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f is one-to-one & rng f = the carrier of Y holds
( (f ") * f = id X & f * (f ") = id Y )