for x, y being ExtReal holds |.(x * y).| = |.x.| * |.y.|