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