theorem Th8: :: NDIFF11:8

for m being non zero Element of NAT
for f being LinearOperator of (REAL-NS m),(REAL-NS m) st f is bijective holds
ex g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m))) st
( g = f & g is invertible )