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 * (((a " ) * ) . y1) by Def1
.= a * ((a " ) * y1) by Def1
.= (a * (a " )) * y1 by GROUP_1:def 4
.= (1_ G) * y1 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