let x, y, z be Element of REAL ; :: thesis: ( x <> 0 & * x,y = 1 & * x,z = 1 implies y = z )
assume that
A1: x <> 0 and
A2: * x,y = 1 and
A3: * x,z = 1 ; :: thesis: y = z
thus y = inv x by A1, A2, Def5
.= z by A1, A3, Def5 ; :: thesis: verum