:: deftheorem defines CosetSet LPSPACE1:def 14 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds CosetSet M = { (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M } ;