theorem IS02A: :: LOPBAN12:13
for E, F, G being RealNormSpace
for u being Lipschitzian BilinearOperator of E,F,G holds u * ((IsoCPNrSP (E,F)) ") is Lipschitzian MultilinearOperator of <*E,F*>,G