reconsider jj = 1 as Element of REAL by NUMBERS:19;
let x, y be Element of REAL ; ( y <> 0 implies * ((* (x,y)),(inv y)) = x )
assume A1:
y <> 0
; * ((* (x,y)),(inv y)) = x
thus * ((* (x,y)),(inv y)) =
* (x,(* (y,(inv y))))
by Th13
.=
* (x,jj)
by A1, Def4
.=
x
by Th19
; verum