:: deftheorem Def39 defines * AIMLOOP:def 41 :
for Q being multLoop
for H being Subset of Q
for x being Element of Q
for b₄ being Subset of Q holds
( b₄ = x * H iff for y being Element of Q holds
( y in b₄ iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) ) );