:: deftheorem defines left-right-mult-closed AIMLOOP:def 38 :
for Q being non empty multLoopStr
for H being Subset of Q
for S being Subset of (Funcs (Q,Q)) holds
( H left-right-mult-closed S iff for u being Element of Q st u in H holds
( (curry the multF of Q) . u in S & (curry' the multF of Q) . u in S ) );