:: deftheorem Def7 defines addCoset ZMODUL02:def 7 :
for V being Z_Module
for W being Submodule of V
for b₃ being BinOp of (CosetSet (V,W)) holds
( b₃ = addCoset (V,W) iff for A, B being Element of CosetSet (V,W)
for a, b being VECTOR of V st A = a + W & B = b + W holds
b₃ . (A,B) = (a + b) + W );