theorem Th43: :: AIMLOOP:46

for Q being multLoop
for N being normal SubLoop of Q holds the carrier of N = (1. Q) * N