let G, H be Group; :: thesis: for a being Element of G
for g being Homomorphism of G,H holds g . (a " ) = (g . a) "
let a be Element of G; :: thesis: for g being Homomorphism of G,H holds g . (a " ) = (g . a) "
let g be Homomorphism of G,H; :: thesis: g . (a " ) = (g . a) "
(g . (a " )) * (g . a) = g . ((a " ) * a) by Def7
.= g . (1_ G) by GROUP_1:def 6
.= 1_ H by Th40 ;
hence g . (a " ) = (g . a) " by GROUP_1:20; :: thesis: verum