theorem Th18: :: RFINSEQ2:18

for R being non-decreasing FinSequence of REAL
for n being Nat holds R | n is non-decreasing FinSequence of REAL