theorem Th32: :: AIMLOOP:35

for Q being multLoop
for H being Subset of Q
for u being Element of Q st u in H holds
(curry the multF of Q) . u in Mlt H