let m be non zero Element of NAT ; :: thesis: 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 )
let f be LinearOperator of (REAL-NS m),(REAL-NS m); :: thesis: ( f is bijective implies ex g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m))) st
( g = f & g is invertible ) )
assume A1: f is bijective ; :: thesis: ex g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m))) st
( g = f & g is invertible )
then consider h being Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS m) such that
A2: ( h = f " & h is one-to-one & h is onto ) by Th7;
( REAL-NS m is finite-dimensional & dim (REAL-NS m) = m ) by REAL_NS2:62;
then f is Lipschitzian by LOPBAN15:2;
then reconsider g = f as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m))) by LOPBAN_1:def 9;
take g ; :: thesis: ( g = f & g is invertible )
thus g = f ; :: thesis: g is invertible
A3: rng g = the carrier of (REAL-NS m) by A1, FUNCT_2:def 3;
h in BoundedLinearOperators ((REAL-NS m),(REAL-NS m)) by LOPBAN_1:def 9;
hence g is invertible by A1, A2, A3, LOPBAN13:def 1; :: thesis: verum