theorem Th47: :: AIMLOOP:50

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