theorem IS01: :: LOPBAN12:7

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