theorem Th25: :: MESFUNC7:25

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds
Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)