theorem IS03A: :: LOPBAN12:14

for X, Y, Z being RealNormSpace ex I being LinearOperator of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)),(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) st
( I is bijective & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds I . u = u * ((IsoCPNrSP (X,Y)) ") ) )