let Q1 be satisfying_aa1 satisfying_aa2 satisfying_aa3 satisfying_aK1 satisfying_aK2 satisfying_aK3 multLoop; :: thesis: 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
let 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 ) & Nucl Q1 c= Ker f holds
Q2 is commutative multGroup
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 ) & Nucl Q1 c= Ker f implies Q2 is commutative multGroup )
assume that
A1: for y being Element of Q2 ex x being Element of Q1 st f . x = y and
A2: Nucl Q1 c= Ker f ; :: thesis: Q2 is commutative multGroup
A3: Q2 is commutative

proof

let x, y be Element of Q2; :: according to GROUP_1:def 12 :: thesis: x * y = y * x
consider x1 being Element of Q1 such that
A4: f . x1 = x by A1;
consider y1 being Element of Q1 such that
A5: f . y1 = y by A1;
K_op (x,y) = 1. Q2

proof

A6: K_op (x1,y1) in Ker f

proof

A7: K_op (x1,y1) in Nucl Q1

proof

now :: thesis: for u, w being Element of Q1 holds (K_op (x1,y1)) * (u * w) = ((K_op (x1,y1)) * u) * w

let u, w be Element of Q1; :: thesis: (K_op (x1,y1)) * (u * w) = ((K_op (x1,y1)) * u) * w
a_op ((K_op (x1,y1)),u,w) = 1. Q1 by Def19;
hence (K_op (x1,y1)) * (u * w) = ((K_op (x1,y1)) * u) * w by Th9; :: thesis: verum

end;

then A8: K_op (x1,y1) in Nucl_l Q1 by Def22;

now :: thesis: for u, w being Element of Q1 holds u * ((K_op (x1,y1)) * w) = (u * (K_op (x1,y1))) * w

let u, w be Element of Q1; :: thesis: u * ((K_op (x1,y1)) * w) = (u * (K_op (x1,y1))) * w
a_op (u,(K_op (x1,y1)),w) = 1. Q1 by Def20;
hence u * ((K_op (x1,y1)) * w) = (u * (K_op (x1,y1))) * w by Th9; :: thesis: verum

end;

then A9: K_op (x1,y1) in Nucl_m Q1 by Def23;

now :: thesis: for u, w being Element of Q1 holds u * (w * (K_op (x1,y1))) = (u * w) * (K_op (x1,y1))

let u, w be Element of Q1; :: thesis: u * (w * (K_op (x1,y1))) = (u * w) * (K_op (x1,y1))
a_op (u,w,(K_op (x1,y1))) = 1. Q1 by Def21;
hence u * (w * (K_op (x1,y1))) = (u * w) * (K_op (x1,y1)) by Th9; :: thesis: verum

end;

then K_op (x1,y1) in Nucl_r Q1 by Def24;
hence K_op (x1,y1) in Nucl Q1 by A8, A9, Th12; :: thesis: verum

end;

thus K_op (x1,y1) in Ker f by A7, A2; :: thesis: verum

end;

K_op (x,y) = (f . (y1 * x1)) \ ((f . x1) * (f . y1)) by Def28b, A4, A5
.= (f . (y1 * x1)) \ (f . (x1 * y1)) by Def28b
.= f . ((y1 * x1) \ (x1 * y1)) by Th13
.= 1. Q2 by A6, Def29 ;
hence K_op (x,y) = 1. Q2 ; :: thesis: verum

end;

hence x * y = y * x by Th10; :: thesis: verum

end;

now :: thesis: for x1, y1, z1 being Element of Q1 holds a_op (x1,y1,z1) in Ker f

let x1, y1, z1 be Element of Q1; :: thesis: a_op (x1,y1,z1) in Ker f
a_op (x1,y1,z1) in Nucl Q1

proof

now :: thesis: for u, w being Element of Q1 holds ((a_op (x1,y1,z1)) * u) * w = (a_op (x1,y1,z1)) * (u * w)

let u, w be Element of Q1; :: thesis: ((a_op (x1,y1,z1)) * u) * w = (a_op (x1,y1,z1)) * (u * w)
a_op ((a_op (x1,y1,z1)),u,w) = 1. Q1 by Def15;
hence ((a_op (x1,y1,z1)) * u) * w = (a_op (x1,y1,z1)) * (u * w) by Th9; :: thesis: verum

end;

then A10: a_op (x1,y1,z1) in Nucl_l Q1 by Def22;

now :: thesis: for u, w being Element of Q1 holds (u * (a_op (x1,y1,z1))) * w = u * ((a_op (x1,y1,z1)) * w)

let u, w be Element of Q1; :: thesis: (u * (a_op (x1,y1,z1))) * w = u * ((a_op (x1,y1,z1)) * w)
a_op (u,(a_op (x1,y1,z1)),w) = 1. Q1 by Def16;
hence (u * (a_op (x1,y1,z1))) * w = u * ((a_op (x1,y1,z1)) * w) by Th9; :: thesis: verum

end;

then A11: a_op (x1,y1,z1) in Nucl_m Q1 by Def23;

now :: thesis: for u, w being Element of Q1 holds (u * w) * (a_op (x1,y1,z1)) = u * (w * (a_op (x1,y1,z1)))

let u, w be Element of Q1; :: thesis: (u * w) * (a_op (x1,y1,z1)) = u * (w * (a_op (x1,y1,z1)))
a_op (u,w,(a_op (x1,y1,z1))) = 1. Q1 by Def17;
hence (u * w) * (a_op (x1,y1,z1)) = u * (w * (a_op (x1,y1,z1))) by Th9; :: thesis: verum

end;

then a_op (x1,y1,z1) in Nucl_r Q1 by Def24;
hence a_op (x1,y1,z1) in Nucl Q1 by A10, A11, Th12; :: thesis: verum

end;

hence a_op (x1,y1,z1) in Ker f by A2; :: thesis: verum

end;

hence Q2 is commutative multGroup by A3, Th15, A1; :: thesis: verum