theorem Th74: :: MEASUR11:3

for F being FinSequence
for n being Nat holds (union (rng (F | n))) \/ (F . (n + 1)) = union (rng (F | (n + 1)))