for v1, v2 being FinSequence of REAL st len v1 = len v2 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2 by Lm15;