theorem Th44: :: AIMLOOP:47

for Q being multLoop
for N being normal SubLoop of Q holds Ker (QuotientHom (Q,N)) = @ ([#] N)