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