let Q1, Q2 be 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
let f be homomorphic Function of Q1,Q2; ( ( 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
; Q2 is associative
thus
Q2 is associative
verumproof
let x,
y,
z be
Element of
Q2;
GROUP_1:def 3 (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;
verum
end;