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