theorem Th6: :: INTEGRA3:6

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