for X, Y, Z being RealNormSpace ex I being LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st
( 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 ) ) ) )