theorem Th63: :: AIMLOOP:66

for Q being AIM multLoop
for x, u being Element of Q st u in Nucl Q holds
(x * u) / x in Nucl Q