:: deftheorem Def11 defines a.e.cpfunc= LPSPACC1:def 11 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX holds
( f a.e.cpfunc= g,M iff ex E being Element of S st
( M . E = 0 & f | (E `) = g | (E `) ) );