let S, T be RealNormSpace; :: thesis: for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds
ex J being LinearOperator of T,S st
( J = I " & J is one-to-one & J is onto & J is isometric )
let I be LinearOperator of S,T; :: thesis: ( I is one-to-one & I is onto & I is isometric implies ex J being LinearOperator of T,S st
( J = I " & J is one-to-one & J is onto & J is isometric ) )
assume that
AS0: ( I is one-to-one & I is onto ) and
AS1: I is isometric ; :: thesis: ex J being LinearOperator of T,S st
( J = I " & J is one-to-one & J is onto & J is isometric )
P0: ( rng I = the carrier of T & dom I = the carrier of S ) by AS0, FUNCT_2:def 1;
P1: ( rng I = dom (I ") & dom I = rng (I ") ) by AS0, FUNCT_1:33;
then reconsider J = I " as Function of T,S by P0, FUNCT_2:1;
X1: for v, w being Point of T holds J . (v + w) = (J . v) + (J . w)

proof

let v, w be Point of T; :: thesis: J . (v + w) = (J . v) + (J . w)
consider t being Point of S such that
X1: v = I . t by AS0, FUNCT_2:113;
consider s being Point of S such that
X2: w = I . s by AS0, FUNCT_2:113;
X3: J . (v + w) = J . (I . (t + s)) by X1, X2, VECTSP_1:def 20
.= t + s by FUNCT_1:34, AS0, P0 ;
J . w = s by X2, FUNCT_1:34, AS0, P0;
hence J . (v + w) = (J . v) + (J . w) by AS0, P0, X1, X3, FUNCT_1:34; :: thesis: verum

end;

X2: for v being Point of T
for r being Real holds J . (r * v) = r * (J . v)

proof

let v be Point of T; :: thesis: for r being Real holds J . (r * v) = r * (J . v)
let r be Real; :: thesis: J . (r * v) = r * (J . v)
consider t being Point of S such that
X1: v = I . t by AS0, FUNCT_2:113;
J . (r * v) = J . (I . (r * t)) by X1, LOPBAN_1:def 5
.= r * t by FUNCT_1:34, AS0, P0 ;
hence J . (r * v) = r * (J . v) by AS0, P0, X1, FUNCT_1:34; :: thesis: verum

end;

reconsider J = J as LinearOperator of T,S by X1, X2, LOPBAN_1:def 5, VECTSP_1:def 20;
take J ; :: thesis: ( J = I " & J is one-to-one & J is onto & J is isometric )
thus J = I " ; :: thesis: ( J is one-to-one & J is onto & J is isometric )
thus ( J is one-to-one & J is onto ) by AS0, P1, FUNCT_2:def 1; :: thesis: J is isometric
for v being Point of T holds ||.(J . v).|| = ||.v.||

proof

let v be Point of T; :: thesis: ||.(J . v).|| = ||.v.||
consider t being Point of S such that
X1: v = I . t by AS0, FUNCT_2:113;
thus ||.(J . v).|| = ||.t.|| by X1, FUNCT_1:34, AS0, P0
.= ||.v.|| by X1, AS1, LMMAZU ; :: thesis: verum

end;

hence J is isometric by LMMAZU; :: thesis: verum