theorem Th53: :: AIMLOOP:56

for Q being multLoop
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 ) )