for p, q being FinSequence of REAL st rng p = rng q & p is increasing & q is increasing holds
p = q