theorem Th86: :: MEMBER_1:86

for f, g being ExtReal holds {f} ** {g} = {(f * g)}