theorem Th55: :: AIMLOOP:58

for Q being multLoop
for f being Function of Q,Q holds
( f in InnAut Q iff ( f in Mlt ([#] Q) & f . (1. Q) = 1. Q ) )