let X, Y be RealNormSpace; :: thesis: for L being LinearOperator of X,Y st L is isomorphism holds
ex K being Lipschitzian LinearOperator of Y,X st
( K = L " & K is isomorphism )

let L be LinearOperator of X,Y; :: thesis: ( L is isomorphism implies ex K being Lipschitzian LinearOperator of Y,X st
( K = L " & K is isomorphism ) )

assume A1: L is isomorphism ; :: thesis: ex K being Lipschitzian LinearOperator of Y,X st
( K = L " & K is isomorphism )

then A2: ( L is one-to-one & L is onto & ( for x being Point of X holds = ||.(L . x).|| ) ) ;
reconsider K = L " as Function of Y,X by ;
A3: dom L = the carrier of X by FUNCT_2:def 1;
A4: K is additive
proof
let x, y be Point of Y; :: according to VECTSP_1:def 19 :: thesis: K . (x + y) = (K . x) + (K . y)
consider a being Point of X such that
A5: x = L . a by ;
consider b being Point of X such that
A6: y = L . b by ;
A7: K . x = a by ;
A8: K . y = b by ;
x + y = L . (a + b) by ;
hence K . (x + y) = (K . x) + (K . y) by ; :: thesis: verum
end;
K is homogeneous
proof
let x be Point of Y; :: according to LOPBAN_1:def 5 :: thesis: for b1 being object holds K . (b1 * x) = b1 * (K . x)
let r be Real; :: thesis: K . (r * x) = r * (K . x)
consider a being Point of X such that
A10: x = L . a by ;
A11: K . x = a by ;
A12: r * x = L . (r * a) by ;
thus K . (r * x) = r * (K . x) by ; :: thesis: verum
end;
then reconsider K = K as LinearOperator of Y,X by A4;
A13: K is onto by ;
A14: for y being Point of Y holds = ||.(K . y).||
proof
let y be Point of Y; :: thesis: = ||.(K . y).||
consider b being Point of X such that
A15: y = L . b by ;
K . y = b by ;
hence ||.y.|| = ||.(K . y).|| by ; :: thesis: verum
end;
then for x being VECTOR of Y holds ||.(K . x).|| <= 1 * ;
then reconsider K = K as Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 8;
take K ; :: thesis: ( K = L " & K is isomorphism )
thus ( K = L " & K is isomorphism ) by ; :: thesis: verum