theorem Th17: :: AIMLOOP:17

for Q1 being satisfying_aa1 satisfying_aa2 satisfying_aa3 satisfying_Ka multLoop
for Q2 being multLoop
for f being homomorphic Function of Q1,Q2 st ( for y being Element of Q2 ex x being Element of Q1 st f . x = y ) & Cent Q1 c= Ker f holds
Q2 is multGroup