theorem Th24: :: AIMLOOP:27

for Q being multLoop holds [#] (lp (Nucl Q)) = Nucl Q