let X, Y be RealNormSpace; :: thesis: ex I being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators ((product <*X*>),Y)) st
( I is one-to-one & I is onto & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for x being Point of X holds (I . u) . <*x*> = u . x ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ||.u.|| = ||.(I . u).|| ) )
set J = IsoCPNrSP X;
consider I being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators ((product <*X*>),Y)) such that
A1: ( I is one-to-one & I is onto & I is isometric & ( for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds I . x = x * ((IsoCPNrSP X) ") ) ) by Th38;
A2: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for x being Point of X holds (I . u) . <*x*> = u . x

proof

let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for x being Point of X holds (I . u) . <*x*> = u . x
let x be Point of X; :: thesis: (I . u) . <*x*> = u . x
A3: (IsoCPNrSP X) . x = <*x*> by Def2;
reconsider px = <*x*> as Point of (product <*X*>) by Th12;
thus (I . u) . <*x*> = (u * ((IsoCPNrSP X) ")) . px by A1
.= u . (((IsoCPNrSP X) ") . px) by FUNCT_2:15
.= u . x by A3, FUNCT_2:26 ; :: thesis: verum

end;

take I ; :: thesis: ( I is one-to-one & I is onto & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for x being Point of X holds (I . u) . <*x*> = u . x ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ||.u.|| = ||.(I . u).|| ) )
thus ( I is one-to-one & I is onto & I is isometric ) by A1; :: thesis: ( ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for x being Point of X holds (I . u) . <*x*> = u . x ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ||.u.|| = ||.(I . u).|| ) )
thus for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for x being Point of X holds (I . u) . <*x*> = u . x by A2; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ||.u.|| = ||.(I . u).||
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ||.u.|| = ||.(I . u).||
thus ||.u.|| = ||.(I . u).|| by A1, NDIFF_7:7; :: thesis: verum