theorem Th25: :: AIMLOOP:28

for Q being multLoop holds [#] (lp (Cent Q)) = Cent Q