:: deftheorem Def15 defines CosOp GROUP_9:def 15 :
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for b₄ being BinOp of (Cosets N) holds
( b₄ = CosOp N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
b₄ = CosOp H );