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