:: deftheorem Def16 defines zeroCoset LPSPACE1:def 16 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being Element of CosetSet M holds
( b₄ = zeroCoset M iff ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b₄ = a.e-eq-class (f,M) ) );