let Q be multLoop; :: thesis:
let x, y be Element of Q; :: thesis:
thus ( x * (lp (Cent Q)) = y * (lp (Cent Q)) implies ex z being Element of Q st
( z in Cent Q & y = x * z ) ) :: thesis:

assume A1: x * (lp (Cent Q)) = y * (lp (Cent Q)) ; :: thesis:
( 1. Q in Cent Q & y = y * (1. Q) ) by Th50;
hence ex z being Element of Q st
( z in Cent Q & y = x * z ) by A1, Th52; :: thesis:

end;

thus ( ex z being Element of Q st
( z in Cent Q & y = x * z ) implies x * (lp (Cent Q)) = y * (lp (Cent Q)) ) :: thesis:

assume ex z being Element of Q st
( z in Cent Q & y = x * z ) ; :: thesis:
then consider z being Element of Q such that
A2: ( z in Cent Q & y = x * z ) ;
z in Nucl Q by A2, XBOOLE_0:def 4;
then A3: z in Nucl_m Q by Th12;
for w being Element of Q holds
( w in x * (lp (Cent Q)) iff w in y * (lp (Cent Q)) )

let w be Element of Q; :: thesis:
thus ( w in x * (lp (Cent Q)) implies w in y * (lp (Cent Q)) ) :: thesis:

assume w in x * (lp (Cent Q)) ; :: thesis:
then consider v being Element of Q such that
A4: ( v in Cent Q & w = x * v ) by Th52;
ex u being Element of Q st
( u in Cent Q & w = y * u )

take z \ v ; :: thesis:
( z in [#] (lp (Cent Q)) & v in [#] (lp (Cent Q)) ) by A2, A4, Th25;
then z \ v in [#] (lp (Cent Q)) by Th39;
hence z \ v in Cent Q by Th25; :: thesis:
w = x * (z * (z \ v)) by A4
.= y * (z \ v) by A2, Def23, A3 ;
hence w = y * (z \ v) ; :: thesis:

end;

hence w in y * (lp (Cent Q)) by Th52; :: thesis:

end;

assume w in y * (lp (Cent Q)) ; :: thesis:
then consider v being Element of Q such that
A5: ( v in Cent Q & w = y * v ) by Th52;
ex u being Element of Q st
( u in Cent Q & w = x * u )

take z * v ; :: thesis:
( z in [#] (lp (Cent Q)) & v in [#] (lp (Cent Q)) ) by A2, A5, Th25;
then z * v in [#] (lp (Cent Q)) by Th37;
hence ( z * v in Cent Q & w = x * (z * v) ) by Def23, A3, A2, A5, Th25; :: thesis:

end;

hence w in x * (lp (Cent Q)) by Th52; :: thesis:

end;

end;