theorem Th15: :: AIMLOOP:15

for Q1, 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 ) & ( for x, y, z being Element of Q1 holds a_op (x,y,z) in Ker f ) holds
Q2 is associative