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 )
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 * (((a ") *) . y1) by Def1
.= a * ((a ") * y1) by Def1
.= (a * (a ")) * y1 by GROUP_1:def 3
.= (1_ G) * y1 by GROUP_1:def 5
.= y by GROUP_1:def 4
.= h . ((h ") . y) by A3, FUNCT_1:35
.= (a *) . (((a *) /") . y) by TOPS_2:def 4 ;
hence ((a *) /") . y = ((a ") *) . y by A4, FUNCT_1:def 4; :: 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:2; :: thesis: verum