:: deftheorem defines * AIMLOOP:def 42 :
for Q being multLoop
for H being SubLoop of Q
for x being Element of Q holds x * H = x * (@ ([#] H));