:: deftheorem defines ./. GROUP_6:def 4 :
for G being Group
for N being normal Subgroup of G holds G ./. N = multMagma(# (Cosets N),(CosOp N) #);