theorem Th30: :: AIMLOOP:33

for Q being multLoop
for u being Element of Q holds (curry the multF of Q) . u is Permutation of Q