theorem Th57: :: MEASURE9:57

for X being non empty set
for F being sequence of X
for n being Nat holds rng (F | (Segm (n + 1))) = (rng (F | (Segm n))) \/ {(F . n)}