theorem Th19: :: MEASURE2:19

for N, F being Function st F . 0 = N . 0 & ( for n being Nat holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
for n, m being Nat st n < m holds
F . n misses F . m