theorem :: LOPBAN14:27

for X, Y being RealNormSpace-Sequence
for Z being RealNormSpace
for f being Lipschitzian BilinearOperator of (product X),(product Y),Z holds f * ((IsoCPNrSP ((product X),(product Y))) ") is Lipschitzian MultilinearOperator of <*(product X),(product Y)*>,Z by LOPBAN12:13;