theorem Th18: :: RFINSEQ2:18

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