theorem Th48: :: AIMLOOP:51

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