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

reconsider h = * a as Function ;
let y be set ; :: thesis: ( y in the carrier of G implies ((* a) /") . y = (* (a ")) . y )
A2: rng (* a) = [#] G by FUNCT_2:def 3;
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 A3: y1 in rng (* a) ;
dom (* a) = the carrier of G by FUNCT_2:def 1;
then A4: ( (* (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 4
.= y1 * (1_ G) by GROUP_1:def 6
.= y by GROUP_1:def 5
.= h . ((h ") . y) by A3, FUNCT_1:57
.= (* a) . (((* a) /") . y) by A2, TOPS_2:def 4 ;
hence ((* a) /") . y = (* (a ")) . y by A4, FUNCT_1:def 8; :: thesis: verum

end;

( dom ((* a) /") = the carrier of G & dom (* (a ")) = the carrier of G ) by FUNCT_2:def 1;
hence (* a) /" = * (a ") by A1, FUNCT_1:9; :: thesis: verum