let G be Group; :: thesis: inverse_op G is one-to-one
set f = inverse_op G;
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: 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 A1: ( x1 in dom (inverse_op G) & x2 in dom (inverse_op G) & (inverse_op G) . x1 = (inverse_op G) . x2 ) ; :: thesis: x1 = x2
then reconsider a = x1, b = x2 as Element of G ;
( (inverse_op G) . a = a " & (inverse_op G) . b = b " ) by GROUP_1:def 7;
hence x1 = x2 by A1, GROUP_1:17; :: thesis: verum