theorem Th22: :: RFINSEQ:22

for R being real-valued FinSequence ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent