:: deftheorem Def37 defines MltClos1 AIMLOOP:def 39 :
for Q being non empty multLoopStr
for H being Subset of Q
for S, b₄ being Subset of (Funcs (Q,Q)) holds
( b₄ = MltClos1 (H,S) iff for f being object holds
( f in b₄ iff ( ex u being Element of Q st
( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st
( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st
( g in S & h in S & f = g * h ) or ex g being Permutation of Q st
( g in S & f = g " ) ) ) );