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)) . y1) + a by Def2
.= (y1 + (- a)) + a by Def2
.= y1 + ((- a) + a) by RLVECT_1:def 3
.= y1 + (0_ G) 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