:: deftheorem defines CCosetSet LPSPACC1:def 15 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds CCosetSet M = { (a.e-Ceq-class (f,M)) where f is PartFunc of X,COMPLEX : f in L1_CFunctions M } ;