theorem :: XXREAL_3:100

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