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