for R being non-increasing FinSequence of REAL
for n being Element of NAT holds R /^ n is non-increasing