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,j) by A1, Def4
.= x by Th19 ; :: thesis: verum