let m be non zero Element of NAT ; :: thesis: 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 )
let f be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m))); :: thesis: for M being Matrix of m,F_Real st f = Mx2Tran M holds
( f is invertible iff Det M <> 0. F_Real )
let M be Matrix of m,F_Real; :: thesis: ( f = Mx2Tran M implies ( f is invertible iff Det M <> 0. F_Real ) )
assume f = Mx2Tran M ; :: thesis: ( f is invertible iff Det M <> 0. F_Real )
then ( f is invertible iff M is invertible ) by Th12;
hence ( f is invertible iff Det M <> 0. F_Real ) by LAPLACE:34; :: thesis: verum