for Q being multLoop
for x, y being Element of Q holds
( y in x * (lp (Cent Q)) iff ex z being Element of Q st
( z in Cent Q & y = x * z ) )