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 Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS m) st
( g = f " & g is one-to-one & g is onto )
let f be LinearOperator of (REAL-NS m),(REAL-NS m); :: thesis: ( f is bijective implies ex g being Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS m) st
( g = f " & g is one-to-one & g is onto ) )
assume f is bijective ; :: thesis: ex g being Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS m) st
( g = f " & g is one-to-one & g is onto )
then consider g being LinearOperator of (REAL-NS m),(REAL-NS m) such that
A2: ( g = f " & g is one-to-one & g is onto ) by REAL_NS2:85;
( REAL-NS m is finite-dimensional & dim (REAL-NS m) = m ) by REAL_NS2:62;
then g is Lipschitzian by LOPBAN15:2;
hence ex g being Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS m) st
( g = f " & g is one-to-one & g is onto ) by A2; :: thesis: verum