theorem Th33: :: AIMLOOP:36

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