:: deftheorem Def18 defines homomorphic GROUP_9:def 18 :
for O being set
for G, H being GroupWithOperators of O
for f being Function of G,H holds
( f is homomorphic iff for o being Element of O
for g being Element of G holds f . ((G ^ o) . g) = (H ^ o) . (f . g) );