theorem :: ARYTM_0:20

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