theorem :: ARYTM_1:26

for x, y, z being Element of REAL+ st z <=' y holds
x *' (y -' z) = (x *' y) - (x *' z)