for R1, R2 being non-decreasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds
R1 = R2