theorem :: GROUP_9:46

for O being set
for G, H being GroupWithOperators of O
for g1 being Element of G
for h being Homomorphism of G,H holds h . (g1 ") = (h . g1) " by Lm13;