theorem :: MYCIELSK:1

for x, y, z being Real st 0 <= x holds
x * (y -' z) = (x * y) -' (x * z)