theorem Th93: :: XXREAL_3:93

for x, y, z being ExtReal st y = - z holds
x * (y + z) = (x * y) + (x * z)