theorem Th96: :: XXREAL_3:96

for x, y, z being ExtReal st y >= 0 & z >= 0 holds
x * (y + z) = (x * y) + (x * z)