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 Th15
.= * (x,j) by A1, Def5
.= x by Th21 ; :: thesis: verum