let Q1, Q2 be multLoop; :: thesis: 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
let f be homomorphic Function of Q1,Q2; :: thesis: ( ( 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 ) implies Q2 is associative )
assume that
A1: for y being Element of Q2 ex x being Element of Q1 st f . x = y and
A2: for x, y, z being Element of Q1 holds a_op (x,y,z) in Ker f ; :: thesis: Q2 is associative
thus Q2 is associative :: thesis: verum

proof

let x, y, z be Element of Q2; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
consider x1 being Element of Q1 such that
A3: f . x1 = x by A1;
consider y1 being Element of Q1 such that
A4: f . y1 = y by A1;
consider z1 being Element of Q1 such that
A5: f . z1 = z by A1;
A6: a_op (x1,y1,z1) in Ker f by A2;
a_op (x,y,z) = ((f . x1) * (f . (y1 * z1))) \ (((f . x1) * (f . y1)) * (f . z1)) by Def28b, A3, A4, A5
.= (f . (x1 * (y1 * z1))) \ (((f . x1) * (f . y1)) * (f . z1)) by Def28b
.= (f . (x1 * (y1 * z1))) \ ((f . (x1 * y1)) * (f . z1)) by Def28b
.= (f . (x1 * (y1 * z1))) \ (f . ((x1 * y1) * z1)) by Def28b
.= f . ((x1 * (y1 * z1)) \ ((x1 * y1) * z1)) by Th13
.= 1. Q2 by A6, Def29 ;
hence (x * y) * z = x * (y * z) by Th9; :: thesis: verum

end;