theorem Th95: :: XXREAL_3:95

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