let G be addGroup; :: thesis: for a being Element of G holds (a +) /" = (- a) +
let a be Element of G; :: thesis: (a +) /" = (- a) +
set f = a + ;
set g = (- a) + ;

A1: now :: thesis: for y being object st y in the carrier of G holds
((a +) /") . y = ((- a) +) . y

reconsider h = a + as Function ;
let y be object ; :: thesis: ( y in the carrier of G implies ((a +) /") . y = ((- a) +) . y )
assume y in the carrier of G ; :: thesis: ((a +) /") . y = ((- a) +) . y
then reconsider y1 = y as Element of G ;
rng (a +) = the carrier of G by FUNCT_2:def 3;
then A2: y1 in rng (a +) ;
dom (a +) = the carrier of G by FUNCT_2:def 1;
then A3: ( ((- a) +) . y1 in dom (a +) & ((a +) /") . y1 in dom (a +) ) ;
(a +) . (((- a) +) . y) = a + (((- a) +) . y1) by Def1
.= a + ((- a) + y1) by Def1
.= (a + (- a)) + y1 by RLVECT_1:def 3
.= (0_ G) + y1 by Def5
.= y by Def4
.= h . ((h ") . y) by A2, FUNCT_1:35
.= (a +) . (((a +) /") . y) by TOPS_2:def 4 ;
hence ((a +) /") . y = ((- a) +) . y by A3, FUNCT_1:def 4; :: thesis: verum

end;

thus (a +) /" = (- a) + by A1; :: thesis: verum