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
( g1 in Ker h iff h . g1 = 1_ H )