:: deftheorem Def15 defines addCoset LPSPACE1:def 15 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being BinOp of (CosetSet M) holds
( b₄ = addCoset M iff for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b₄ . (A,B) = a.e-eq-class ((a + b),M) );