theorem Th12: :: NDIFF11:12

for m being non zero Element of NAT
for f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m)))
for M being Matrix of m,F_Real st f = Mx2Tran M holds
( f is invertible iff M is invertible )