let S, T, W be RealNormSpace; :: thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators (S,W))
for g being Point of (R_NormSpace_of_BoundedLinearOperators (T,W))
for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric & f = g * I holds
||.f.|| = ||.g.||
let f be Point of (R_NormSpace_of_BoundedLinearOperators (S,W)); :: thesis: for g being Point of (R_NormSpace_of_BoundedLinearOperators (T,W))
for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric & f = g * I holds
||.f.|| = ||.g.||
let g be Point of (R_NormSpace_of_BoundedLinearOperators (T,W)); :: thesis: for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric & f = g * I holds
||.f.|| = ||.g.||
let I be LinearOperator of S,T; :: thesis: ( I is one-to-one & I is onto & I is isometric & f = g * I implies ||.f.|| = ||.g.|| )
assume AS: ( I is one-to-one & I is onto & I is isometric & f = g * I ) ; :: thesis: ||.f.|| = ||.g.||
P1: dom I = the carrier of S by FUNCT_2:def 1;
consider J being LinearOperator of T,S such that
P2: ( J = I " & J is one-to-one & J is onto & J is isometric ) by AS, LM020;
reconsider f0 = f as Lipschitzian LinearOperator of S,W by LOPBAN_1:def 9;
reconsider g0 = g as Lipschitzian LinearOperator of T,W by LOPBAN_1:def 9;
reconsider gI = g * I as Lipschitzian LinearOperator of S,W by LOPBAN_1:def 9, AS;
Y1: for x being object holds
( x in { ||.(g0 . t).|| where t is VECTOR of T : ||.t.|| <= 1 } iff x in { ||.(gI . w).|| where w is VECTOR of S : ||.w.|| <= 1 } )

proof

let x be object ; :: thesis: ( x in { ||.(g0 . t).|| where t is VECTOR of T : ||.t.|| <= 1 } iff x in { ||.(gI . w).|| where w is VECTOR of S : ||.w.|| <= 1 } )

hereby :: thesis: ( x in { ||.(gI . w).|| where w is VECTOR of S : ||.w.|| <= 1 } implies x in { ||.(g0 . t).|| where t is VECTOR of T : ||.t.|| <= 1 } )

assume x in { ||.(g0 . t).|| where t is VECTOR of T : ||.t.|| <= 1 } ; :: thesis: x in { ||.(gI . w).|| where w is VECTOR of S : ||.w.|| <= 1 }
then consider t being VECTOR of T such that
B1: ( x = ||.(g0 . t).|| & ||.t.|| <= 1 ) ;
set s = J . t;
B2: gI . (J . t) = g0 . (I . (J . t)) by P1, FUNCT_1:13
.= g0 . t by FUNCT_1:35, AS, P2 ;
||.(J . t).|| <= 1 by B1, P2, LMMAZU;
hence x in { ||.(gI . w).|| where w is VECTOR of S : ||.w.|| <= 1 } by B1, B2; :: thesis: verum

end;

assume x in { ||.(gI . w).|| where w is VECTOR of S : ||.w.|| <= 1 } ; :: thesis: x in { ||.(g0 . t).|| where t is VECTOR of T : ||.t.|| <= 1 }
then consider w being VECTOR of S such that
B1: ( x = ||.(gI . w).|| & ||.w.|| <= 1 ) ;
set t = I . w;
B2: gI . w = g0 . (I . w) by P1, FUNCT_1:13;
||.(I . w).|| <= 1 by B1, AS, LMMAZU;
hence x in { ||.(g0 . t).|| where t is VECTOR of T : ||.t.|| <= 1 } by B1, B2; :: thesis: verum

end;

X0: PreNorms f0 = PreNorms g0 by AS, Y1, TARSKI:2;
X1: PreNorms (modetrans (f,S,W)) = PreNorms f0 by LOPBAN_1:29
.= PreNorms (modetrans (g,T,W)) by X0, LOPBAN_1:29 ;
thus ||.f.|| = upper_bound (PreNorms (modetrans (f,S,W))) by LOPBAN_1:def 13
.= ||.g.|| by X1, LOPBAN_1:def 13 ; :: thesis: verum