for Q, Q2 being multLoop
for f being homomorphic Function of Q,Q2
for x, y being Element of Q holds
( y in x * (Ker f) iff f . x = f . y )