theorem Th4: :: MEASURE2:4

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)) \/ (F . n) ) )