theorem :: NDIFF11:13

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 Det M <> 0. F_Real )