theorem :: RFINSEQ:21

for R being real-valued non-increasing FinSequence
for n being Nat holds R /^ n is non-increasing