:: deftheorem Def46 defines Coset_Loop_Op AIMLOOP:def 48 :
for Q being multLoop
for N being normal SubLoop of Q
for b₃ being BinOp of (Cosets N) holds
( b₃ = Coset_Loop_Op N iff for H1, H2 being Element of Cosets N holds b₃ . (H1,H2) = H1 * H2 );