:: deftheorem defines _/_ AIMLOOP:def 49 :
for Q being multLoop
for N being normal SubLoop of Q holds Q _/_ N = multLoopStr(# (Cosets N),(Coset_Loop_Op N),(SubLoop_As_Coset N) #);