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

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 Cent Q1

proof

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

let u be Element of Q1; :: thesis: (a_op (x1,y1,z1)) * u = u * (a_op (x1,y1,z1))
K_op ((a_op (x1,y1,z1)),u) = 1. Q1 by Def18;
hence (a_op (x1,y1,z1)) * u = u * (a_op (x1,y1,z1)) by Th10; :: thesis: verum

end;

then A3: a_op (x1,y1,z1) in Comm Q1 by Def25;

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 A4: 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 A5: 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;
then a_op (x1,y1,z1) in Nucl Q1 by A4, A5, Th12;
hence a_op (x1,y1,z1) in Cent Q1 by A3, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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