for x, y, z being Element of REAL st x <> 0 & * (x,y) = 1 & * (x,z) = 1 holds
y = z