theorem IS01A: :: LOPBAN12:12

for E, F, G being RealNormSpace
for u being Lipschitzian MultilinearOperator of <*E,F*>,G holds u * (IsoCPNrSP (E,F)) is Lipschitzian BilinearOperator of E,F,G