let O be set ; :: thesis: for G, H being GroupWithOperators of O

for a being Element of G

for g being Homomorphism of G,H holds g . (a ") = (g . a) "

let G, H be GroupWithOperators of O; :: 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 GROUP_6:def 6

.= g . (1_ G) by GROUP_1:def 5

.= 1_ H by Lm12 ;

hence g . (a ") = (g . a) " by GROUP_1:12; :: thesis: verum

for a being Element of G

for g being Homomorphism of G,H holds g . (a ") = (g . a) "

let G, H be GroupWithOperators of O; :: 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 GROUP_6:def 6

.= g . (1_ G) by GROUP_1:def 5

.= 1_ H by Lm12 ;

hence g . (a ") = (g . a) " by GROUP_1:12; :: thesis: verum