for x, y being Element of REAL st + ((* (x,x)),(* (y,y))) = 0 holds
x = 0