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