theorem Th16: :: MEASURE3:16

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of (COM (S,M))
for G being sequence of S ex H being sequence of (bool X) st
for n being Element of NAT holds H . n = (F . n) \ (G . n)