let X, Y, Z be RealNormSpace; :: thesis: ex I being LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) st
( I is bijective & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(I . u).|| & ( for x being Point of X
for y being Point of Y holds (I . u) . <*x,y*> = (u . x) . y ) ) ) )
consider I being LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) such that
A1: ( I is bijective & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(I . u).|| & ( for x being Point of X
for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) ) ) ) by LOPBAN_9:27;
consider J being LinearOperator of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)),(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) such that
A2: ( J is bijective & J is isometric & ( for u being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds J . u = u * ((IsoCPNrSP (X,Y)) ") ) ) by IS03A;
reconsider K = J * I as LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) by LOPBAN_2:1;
take K ; :: thesis: ( K is bijective & K is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(K . u).|| & ( for x being Point of X
for y being Point of Y holds (K . u) . <*x,y*> = (u . x) . y ) ) ) )
thus K is bijective by A1, A2, FUNCT_2:27; :: thesis: ( K is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(K . u).|| & ( for x being Point of X
for y being Point of Y holds (K . u) . <*x,y*> = (u . x) . y ) ) ) )
A3: for x being Element of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds ||.(K . x).|| = ||.x.||
proof
let x be Element of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))); :: thesis: ||.(K . x).|| = ||.x.||
thus ||.(K . x).|| = ||.(J . (I . x)).|| by FUNCT_2:15
.= ||.(I . x).|| by A2, NDIFF_7:7
.= ||.x.|| by A1 ; :: thesis: verum
end;
hence K is isometric by NDIFF_7:7; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(K . u).|| & ( for x being Point of X
for y being Point of Y holds (K . u) . <*x,y*> = (u . x) . y ) )
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))); :: thesis: ( ||.u.|| = ||.(K . u).|| & ( for x being Point of X
for y being Point of Y holds (K . u) . <*x,y*> = (u . x) . y ) )
thus ||.(K . u).|| = ||.u.|| by A3; :: thesis: for x being Point of X
for y being Point of Y holds (K . u) . <*x,y*> = (u . x) . y
let x be Point of X; :: thesis: for y being Point of Y holds (K . u) . <*x,y*> = (u . x) . y
let y be Point of Y; :: thesis: (K . u) . <*x,y*> = (u . x) . y
A4: K . u = J . (I . u) by FUNCT_2:15;
reconsider xy = <*x,y*> as Point of (product <*X,Y*>) by PRVECT_3:19;
thus (K . u) . <*x,y*> = ((I . u) * ((IsoCPNrSP (X,Y)) ")) . xy by A2, A4
.= (I . u) . (((IsoCPNrSP (X,Y)) ") . xy) by FUNCT_2:15
.= (I . u) . (x,y) by NDIFF_7:18
.= (u . x) . y by A1 ; :: thesis: verum