for r1, r2 being Real st |[r1]| = |[r2]| holds
r1 = r2 by FINSEQ_1:76;