let G be Group; :: 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 GROUP_1:def 3
.= y1 * (1_ G) by GROUP_1:def 5
.= y by GROUP_1:def 4
.= 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