theorem :: ARYTM_1:28

for x, y, z being Element of REAL+ st y -' z <> {} & z <=' y & x <> {} holds
(x *' z) - (x *' y) = [{},(x *' (y -' z))]