theorem Th6: :: MEASURE2:6

for X being set
for S being non empty Subset-Family of X
for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for n, m being Nat st n < m holds
F . n c= F . m