theorem Th21: :: AIMLOOP:24

for Q being multLoop
for x, y being Element of Q st x in Nucl Q & y in Nucl Q holds
x * y in Nucl Q