:: deftheorem Def8 defines addCoset LPSPACE2:def 8 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real
for b₅ being BinOp of (CosetSet (M,k)) holds
( b₅ = addCoset (M,k) iff for A, B being Element of CosetSet (M,k)
for a, b being PartFunc of X,REAL st a in A & b in B holds
b₅ . (A,B) = a.e-eq-class_Lp ((a + b),M,k) );