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 M is invertible )
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 M is invertible )
let M be Matrix of m,F_Real; :: thesis: ( f = Mx2Tran M implies ( f is invertible iff M is invertible ) )
assume A1: f = Mx2Tran M ; :: thesis: ( f is invertible iff M is invertible )
A2: the carrier of (TOP-REAL m) = REAL m by EUCLID:22;
A3: the carrier of (REAL-NS m) = REAL m by REAL_NS1:def 4;

hereby :: thesis: ( M is invertible implies f is invertible )

assume f is invertible ; :: thesis: M is invertible
then ( Mx2Tran M is one-to-one & rng (Mx2Tran M) = the carrier of (REAL-NS m) ) by A1, LOPBAN13:def 1;
then Mx2Tran M is bijective by A2, A3, FUNCT_2:def 3;
hence M is invertible by Th10; :: thesis: verum

end;

assume M is invertible ; :: thesis: f is invertible
then Mx2Tran M is bijective by Th10;
then ( f is one-to-one & rng f = the carrier of (REAL-NS m) ) by A1, A2, A3, FUNCT_2:def 3;
hence f is invertible by Th11; :: thesis: verum