let G be Group; :: thesis: inverse_op G is one-to-one
set f = inverse_op G;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (inverse_op G) or not x2 in dom (inverse_op G) or not (inverse_op G) . x1 = (inverse_op G) . x2 or x1 = x2 )
assume that
A1: ( x1 in dom (inverse_op G) & x2 in dom (inverse_op G) ) and
A2: (inverse_op G) . x1 = (inverse_op G) . x2 ; :: thesis: x1 = x2
reconsider a = x1, b = x2 as Element of G by A1;
( (inverse_op G) . a = a " & (inverse_op G) . b = b " ) by GROUP_1:def 6;
hence x1 = x2 by A2, GROUP_1:9; :: thesis: verum