theorem Th27: :: ARYTM_1:27

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