theorem Th19: :: RFINSEQ2:19

for R1, R2 being real-valued non-decreasing FinSequence st R1,R2 are_fiberwise_equipotent holds
R1 = R2