theorem Th51: :: AIMLOOP:54
for Q being multLoop
for f being Function of Q,Q st f in Mlt (Cent Q) holds
ex z being Element of Q st
( z in Cent Q & ( for x being Element of Q holds f . x = x * z ) )