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