let Q be multLoop; :: thesis: for x, y being Element of Q holds
( x * (lp (Cent Q)) = y * (lp (Cent Q)) iff ex z being Element of Q st
( z in Cent Q & y = x * z ) )
let x, y be Element of Q; :: thesis: ( x * (lp (Cent Q)) = y * (lp (Cent Q)) iff ex z being Element of Q st
( z in Cent Q & y = x * z ) )
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: ( ex z being Element of Q st
( z in Cent Q & y = x * z ) implies x * (lp (Cent Q)) = y * (lp (Cent Q)) )

proof

assume A1: x * (lp (Cent Q)) = y * (lp (Cent Q)) ; :: thesis: ex z being Element of Q st
( z in Cent Q & y = x * z )
( 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: verum

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: verum

proof

assume ex z being Element of Q st
( z in Cent Q & y = x * z ) ; :: thesis: x * (lp (Cent Q)) = y * (lp (Cent Q))
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)) )

proof

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

proof

assume w in x * (lp (Cent Q)) ; :: thesis: w in y * (lp (Cent Q))
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 )

proof

take z \ v ; :: thesis: ( z \ v in Cent Q & w = y * (z \ v) )
( 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 = y * (z \ v)
w = x * (z * (z \ v)) by A4
.= y * (z \ v) by A2, Def23, A3 ;
hence w = y * (z \ v) ; :: thesis: verum

end;

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

end;

assume w in y * (lp (Cent Q)) ; :: thesis: w in x * (lp (Cent Q))
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 )

proof

take z * v ; :: thesis: ( z * v in Cent Q & w = x * (z * v) )
( 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: verum

end;

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

end;

hence x * (lp (Cent Q)) = y * (lp (Cent Q)) by SUBSET_1:3; :: thesis: verum

end;