:: deftheorem Def44 defines normal AIMLOOP:def 46 :
for Q being multLoop
for H being SubLoop of Q holds
( H is normal iff for x, y being Element of Q holds
( (x * H) * (y * H) = (x * y) * H & ( for z being Element of Q holds
( ( (x * H) * (y * H) = (x * H) * (z * H) implies y * H = z * H ) & ( (y * H) * (x * H) = (z * H) * (x * H) implies y * H = z * H ) ) ) ) );