theorem :: LOPBAN14:28

for X, Y being RealNormSpace-Sequence
for Z being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedBilinearOperators ((product X),(product Y),Z)) holds f * ((IsoCPNrSP ((product X),(product Y))) ") is Point of (R_NormSpace_of_BoundedMultilinearOperators (<*(product X),(product Y)*>,Z))