let X, Y be RealNormSpace; :: thesis: 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 )
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( f is one-to-one & rng f = the carrier of Y implies ( (f ") * f = id X & f * (f ") = id Y ) )
assume A1: ( f is one-to-one & rng f = the carrier of Y ) ; :: thesis: ( (f ") * f = id X & f * (f ") = id Y )
A2: f is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
hence (f ") * f = id X by A1, FUNCT_2:29; :: thesis: f * (f ") = id Y
thus f * (f ") = id Y by A1, A2, FUNCT_2:29; :: thesis: verum