:: deftheorem Def42 defines * AIMLOOP:def 44 :
for Q being multLoopStr
for H1, H2, b₄ being Subset of Q holds
( b₄ = H1 * H2 iff for x being Element of Q holds
( x in b₄ iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) ) );