theorem Th22: :: RFINSEQ:22

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