theorem Th20: :: MESFUN12:20

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 holds Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)