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 st f in L1_CFunctions M & g in L1_CFunctions M & f a.e.cpfunc= g,M holds
( |.f.| a.e.= |.g.|,M & Integral (M,|.f.|) = Integral (M,|.g.|) )