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