theorem IS02: :: LOPBAN12:8

for E, F, G being RealLinearSpace
for u being BilinearOperator of E,F,G holds u * ((IsoCPRLSP (E,F)) ") is MultilinearOperator of <*E,F*>,G