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 (X,Y)),(R_NormSpace_of_BoundedLinearOperators (X,Z)) st
( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds L . f = I * f ) )
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 (X,Y)),(R_NormSpace_of_BoundedLinearOperators (X,Z)) st
( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds L . f = I * f ) ) )
assume A1: ( I is one-to-one & I is onto & I is isometric ) ; :: thesis: ex L being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (X,Z)) st
( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds L . f = I * f ) )
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 (X,Y));
set G = the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z));
defpred S₁[ Function, Function] means $2 = I * $1;
A4: for f being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ex g being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) st S₁[f,g]

proof

let f be Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ex g being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) st S₁[f,g]
reconsider f = f as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
I * f is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2;
then reconsider g = I * f as Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) 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 (X,Y)), the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) such that
A5: for f being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (X,Y)) & f2 in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) & L . f1 = L . f2 holds
f1 = f2

proof

let f1, f2 be object ; :: thesis: ( f1 in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) & f2 in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) & L . f1 = L . f2 implies f1 = f2 )
assume A7: ( f1 in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) & f2 in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) & L . f1 = L . f2 ) ; :: thesis: f1 = f2
then reconsider u1 = f1, u2 = f2 as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ;
reconsider v1 = u1, v2 = u2 as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
L . v1 = I * v1 by A5;
then I * v1 = I * v2 by A5, A7;
then J * (I * v1) = (J * I) * v2 by RELAT_1:36;
then A8: (J * I) * v1 = (J * I) * v2 by RELAT_1:36;
A9: J * I = id the carrier of Y by A1, A2, FUNCT_2:29;
then (J * I) * v1 = 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 (X,Z)) holds
ex f being object st
( f in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) & g = L . f )

proof

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

end;

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

proof

let f1, f2 be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: L . (f1 + f2) = (L . f1) + (L . f2)
reconsider ff1 = f1, ff2 = f2, f12 = f1 + f2 as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
A13: L . f1 = I * f1 by A5;
A14: L . f2 = I * f2 by A5;
A15: L . (f1 + f2) = I * (f1 + f2) by A5;
set g1 = L . f1;
set g2 = L . f2;
set g12 = L . (f1 + f2);
for x being VECTOR of X holds (L . (f1 + f2)) . x = ((L . f1) . x) + ((L . f2) . x)

proof

let x be VECTOR of X; :: thesis: (L . (f1 + f2)) . x = ((L . f1) . x) + ((L . f2) . x)
A16: (L . f1) . x = I . (ff1 . x) by A13, FUNCT_2:15;
A17: (L . f2) . x = I . (ff2 . x) by A14, FUNCT_2:15;
(L . (f1 + f2)) . x = I . (f12 . x) by A15, FUNCT_2:15
.= I . ((ff1 . x) + (ff2 . x)) by LOPBAN_1:35 ;
hence (L . (f1 + f2)) . x = ((L . f1) . x) + ((L . f2) . x) by A16, A17, VECTSP_1:def 20; :: 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 (X,Y))
for a being Real holds L . (a * f) = a * (L . f)

proof

let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: 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 X,Y by LOPBAN_1:def 9;
A18: L . f = I * f by A5;
A19: L . (a * f) = I * (a * f) by A5;
set g = L . f;
set ag = L . (a * f);
for t being VECTOR of X holds (L . (a * f)) . t = a * ((L . f) . t)

proof

let t be VECTOR of X; :: thesis: (L . (a * f)) . t = a * ((L . f) . t)
A20: (L . f) . t = I . (f1 . t) by A18, FUNCT_2:15;
(L . (a * f)) . t = I . (af . t) by A19, FUNCT_2:15
.= I . (a * (f . t)) by LOPBAN_1:36 ;
hence (L . (a * f)) . t = a * ((L . f) . t) by A20, LOPBAN_1:def 5; :: 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 (X,Y)),(R_NormSpace_of_BoundedLinearOperators (X,Z)) by A12, LOPBAN_1:def 5, VECTSP_1:def 20;
A21: for f being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ||.(L . f).|| = ||.f.||

proof

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

proof

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

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

assume z in PreNorms f1 ; :: thesis: z in PreNorms g
then consider x being VECTOR of X such that
A24: ( z = ||.(f1 . x).|| & ||.x.|| <= 1 ) ;
g = I * f by A5;
then ||.(g . x).|| = ||.(I . (f1 . x)).|| by FUNCT_2:15
.= ||.(f1 . x).|| by A1, NDIFF_7:7 ;
hence z in PreNorms g by A24; :: thesis: verum

end;

assume z in PreNorms g ; :: thesis: z in PreNorms f1
then consider x being VECTOR of X such that
A25: ( z = ||.(g . x).|| & ||.x.|| <= 1 ) ;
||.(g . x).|| = ||.((I * f1) . x).|| by A5
.= ||.(I . (f1 . x)).|| by FUNCT_2:15
.= ||.(f1 . x).|| by NDIFF_7:7, A1 ;
hence z in PreNorms f1 by A25; :: thesis: verum

end;

hence ||.(L . f).|| = ||.f.|| by A22, A23, 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 (X,Y)),(R_NormSpace_of_BoundedLinearOperators (X,Z)) ;
take L ; :: thesis: ( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds L . f = I * f ) )
thus ( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds L . f = I * f ) ) by A5, A10, A21, NDIFF_7:7, A6, FUNCT_2:10, FUNCT_2:19; :: thesis: verum