let m be non zero Element of NAT ; :: thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m))) st f is one-to-one & rng f = the carrier of (REAL-NS m) holds
f is invertible
let f be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m))); :: thesis: ( f is one-to-one & rng f = the carrier of (REAL-NS m) implies f is invertible )
assume A1: ( f is one-to-one & rng f = the carrier of (REAL-NS m) ) ; :: thesis: f is invertible
reconsider g = f as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS m) by LOPBAN_1:def 9;
g is bijective by A1, FUNCT_2:def 3;
then ex f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m))) st
( f = g & f is invertible ) by Th8;
hence f is invertible ; :: thesis: verum