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