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