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