:: deftheorem Def3 defines CosOp GROUP_6:def 3 :
for G being Group
for N being normal Subgroup of G
for b₃ being BinOp of (Cosets N) holds
( b₃ = CosOp N iff for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b₃ . (W1,W2) = A1 * A2 );