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