for Q1 being satisfying_aa1 satisfying_aa2 satisfying_aa3 satisfying_aK1 satisfying_aK2 satisfying_aK3 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 ) & Nucl Q1 c= Ker f holds
Q2 is commutative multGroup