theorem :: EXTREAL1:19

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