theorem :: XXREAL_3:97

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