let X, Y, Z be RealNormSpace; :: thesis: for I being Lipschitzian LinearOperator of Y,Z st I is one-to-one & I is onto & I is isometric holds
ex L being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (Z,X)) st
( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) holds L . f = f * (I ") ) )
let I be Lipschitzian LinearOperator of Y,Z; :: thesis: ( I is one-to-one & I is onto & I is isometric implies ex L being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (Z,X)) st
( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) holds L . f = f * (I ") ) ) )
assume A1: ( I is one-to-one & I is onto & I is isometric ) ; :: thesis: ex L being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (Z,X)) st
( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) holds L . f = f * (I ") ) )
then consider J being LinearOperator of Z,Y such that
A2: J = I " and
( J is one-to-one & J is onto ) and
A3: J is isometric by NDIFF_7:9;
reconsider J = J as Lipschitzian LinearOperator of Z,Y by A3;
set F = the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X));
set G = the carrier of (R_NormSpace_of_BoundedLinearOperators (Z,X));
defpred S₁[ Function, Function] means $2 = $1 * J;
A4: for f being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) ex g being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (Z,X)) st S₁[f,g]

proof

let f be Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)); :: thesis: ex g being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (Z,X)) st S₁[f,g]
reconsider f1 = f as Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 9;
f1 * J is Lipschitzian LinearOperator of Z,X by LOPBAN_2:2;
then reconsider g = f1 * J as Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (Z,X)) by LOPBAN_1:def 9;
take g ; :: thesis: S₁[f,g]
thus S₁[f,g] ; :: thesis: verum

end;

consider L being Function of the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)), the carrier of (R_NormSpace_of_BoundedLinearOperators (Z,X)) such that
A5: for f being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) holds S₁[f,L . f] from FUNCT_2:sch 3(A4);
A6: for f1, f2 being object st f1 in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) & f2 in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) & L . f1 = L . f2 holds
f1 = f2

proof

let f1, f2 be object ; :: thesis: ( f1 in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) & f2 in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) & L . f1 = L . f2 implies f1 = f2 )
assume A7: ( f1 in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) & f2 in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) & L . f1 = L . f2 ) ; :: thesis: f1 = f2
then reconsider u1 = f1, u2 = f2 as Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) ;
reconsider v1 = u1, v2 = u2 as Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 9;
L . v1 = v1 * J by A5;
then v1 * J = v2 * J by A5, A7;
then (v1 * J) * I = v2 * (J * I) by RELAT_1:36;
then A8: v1 * (J * I) = v2 * (J * I) by RELAT_1:36;
A9: J * I = id the carrier of Y by A1, A2, FUNCT_2:29;
then v1 * (J * I) = v1 by FUNCT_2:17;
hence f1 = f2 by A8, A9, FUNCT_2:17; :: thesis: verum

end;

A10: for g being object st g in the carrier of (R_NormSpace_of_BoundedLinearOperators (Z,X)) holds
ex f being object st
( f in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) & g = L . f )

proof

let g be object ; :: thesis: ( g in the carrier of (R_NormSpace_of_BoundedLinearOperators (Z,X)) implies ex f being object st
( f in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) & g = L . f ) )
assume g in the carrier of (R_NormSpace_of_BoundedLinearOperators (Z,X)) ; :: thesis: ex f being object st
( f in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) & g = L . f )
then reconsider g1 = g as Point of (R_NormSpace_of_BoundedLinearOperators (Z,X)) ;
reconsider g2 = g1 as Lipschitzian LinearOperator of Z,X by LOPBAN_1:def 9;
reconsider f1 = g2 * I as Lipschitzian LinearOperator of Y,X by LOPBAN_2:2;
reconsider f = f1 as Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) by LOPBAN_1:def 9;
take f ; :: thesis: ( f in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) & g = L . f )
thus f in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) ; :: thesis: g = L . f
A11: I * J = id the carrier of Z by A1, A2, FUNCT_2:29;
thus L . f = (g2 * I) * J by A5
.= g2 * (I * J) by RELAT_1:36
.= g by A11, FUNCT_2:17 ; :: thesis: verum

end;

A12: for f1, f2 being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) holds L . (f1 + f2) = (L . f1) + (L . f2)

proof

let f1, f2 be Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)); :: thesis: L . (f1 + f2) = (L . f1) + (L . f2)
reconsider u1 = f1, u2 = f2, u12 = f1 + f2 as Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 9;
A13: L . f1 = f1 * J by A5;
A14: L . f2 = f2 * J by A5;
A15: L . (f1 + f2) = (f1 + f2) * J by A5;
set g1 = L . f1;
set g2 = L . f2;
set g12 = L . (f1 + f2);
for z being VECTOR of Z holds (L . (f1 + f2)) . z = ((L . f1) . z) + ((L . f2) . z)

proof

let z be VECTOR of Z; :: thesis: (L . (f1 + f2)) . z = ((L . f1) . z) + ((L . f2) . z)
A16: (L . f2) . z = u2 . (J . z) by A14, FUNCT_2:15;
(L . (f1 + f2)) . z = u12 . (J . z) by A15, FUNCT_2:15
.= (u1 . (J . z)) + (u2 . (J . z)) by LOPBAN_1:35 ;
hence (L . (f1 + f2)) . z = ((L . f1) . z) + ((L . f2) . z) by A13, FUNCT_2:15, A16; :: thesis: verum

end;

hence L . (f1 + f2) = (L . f1) + (L . f2) by LOPBAN_1:35; :: thesis: verum

end;

for f being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X))
for a being Real holds L . (a * f) = a * (L . f)

proof

let f be Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)); :: thesis: for a being Real holds L . (a * f) = a * (L . f)
let a be Real; :: thesis: L . (a * f) = a * (L . f)
reconsider f1 = f, af = a * f as Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 9;
A17: L . f = f * J by A5;
A18: L . (a * f) = (a * f) * J by A5;
set g = L . f;
set ag = L . (a * f);
for t being VECTOR of Z holds (L . (a * f)) . t = a * ((L . f) . t)

proof

let t be VECTOR of Z; :: thesis: (L . (a * f)) . t = a * ((L . f) . t)
(L . (a * f)) . t = af . (J . t) by A18, FUNCT_2:15
.= a * (f1 . (J . t)) by LOPBAN_1:36 ;
hence (L . (a * f)) . t = a * ((L . f) . t) by A17, FUNCT_2:15; :: thesis: verum

end;

hence L . (a * f) = a * (L . f) by LOPBAN_1:36; :: thesis: verum

end;

then reconsider L = L as LinearOperator of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (Z,X)) by A12, LOPBAN_1:def 5, VECTSP_1:def 20;
A19: for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,X)) holds ||.(L . f).|| = ||.f.||

proof

let f be Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)); :: thesis: ||.(L . f).|| = ||.f.||
reconsider f1 = f as Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 9;
reconsider g = L . f as Lipschitzian LinearOperator of Z,X by LOPBAN_1:def 9;
A20: ||.f.|| = (BoundedLinearOperatorsNorm (Y,X)) . f by NORMSP_0:def 1
.= upper_bound (PreNorms f1) by LOPBAN_1:30 ;
A21: ||.(L . f).|| = (BoundedLinearOperatorsNorm (Z,X)) . g by NORMSP_0:def 1
.= upper_bound (PreNorms g) by LOPBAN_1:30 ;
for n being object holds
( n in PreNorms f1 iff n in PreNorms g )

proof

let n be object ; :: thesis: ( n in PreNorms f1 iff n in PreNorms g )

hereby :: thesis: ( n in PreNorms g implies n in PreNorms f1 )

assume n in PreNorms f1 ; :: thesis: n in PreNorms g
then consider y being VECTOR of Y such that
A22: ( n = ||.(f1 . y).|| & ||.y.|| <= 1 ) ;
g = f * J by A5;
then A23: ||.(g . (I . y)).|| = ||.(f1 . (J . (I . y))).|| by FUNCT_2:15
.= ||.(f1 . y).|| by A1, A2, FUNCT_2:26 ;
||.(I . y).|| = ||.y.|| by A1, NDIFF_7:7;
hence n in PreNorms g by A23, A22; :: thesis: verum

end;

assume n in PreNorms g ; :: thesis: n in PreNorms f1
then consider z being VECTOR of Z such that
A24: ( n = ||.(g . z).|| & ||.z.|| <= 1 ) ;
A25: ||.(g . z).|| = ||.((f1 * J) . z).|| by A5
.= ||.(f1 . (J . z)).|| by FUNCT_2:15 ;
||.(J . z).|| = ||.z.|| by A3, NDIFF_7:7;
hence n in PreNorms f1 by A24, A25; :: thesis: verum

end;

hence ||.(L . f).|| = ||.f.|| by A20, A21, TARSKI:2; :: thesis: verum

end;

then L is isometric by NDIFF_7:7;
then reconsider L = L as Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (Z,X)) ;
take L ; :: thesis: ( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) holds L . f = f * (I ") ) )
thus ( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) holds L . f = f * (I ") ) ) by A2, A5, A6, A10, A19, NDIFF_7:7, FUNCT_2:10, FUNCT_2:19; :: thesis: verum