theorem Th19: :: AIMLOOP:19

for Q, Q2 being multLoop
for f being homomorphic Function of Q,Q2 holds [#] (lp (Ker f)) = Ker f