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