theorem Th11: :: NDIFF11:11

for m being non zero Element of NAT
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