theorem Th35: :: AIMLOOP:38

for Q being multLoop
for H being Subset of Q
for f being Element of Funcs (Q,Q) st f in Mlt H holds
f is Permutation of Q