:: deftheorem Def50 defines AIM AIMLOOP:def 52 :
for Q being multLoop holds
( Q is AIM iff for f, g being Function of Q,Q st f in InnAut Q & g in InnAut Q holds
f * g = g * f );