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