theorem :: GROUP_9:45

for O being set
for G, H being GroupWithOperators of O
for h being Homomorphism of G,H holds h . (1_ G) = 1_ H by Lm12;