theorem :: ARYTM_0:22

for x, y being Element of REAL holds inv (* (x,y)) = * ((inv x),(inv y))