theorem Th6: :: AIMLOOP:6

for Q being multLoop
for x being Element of Q holds x / x = 1. Q