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, Def4
.= z by A1, A3, Def4 ; :: thesis: verum