theorem Th3: :: MEASURE2:3

for X being set
for S being SigmaField of X
for N being sequence of S ex F being sequence of S st
( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )