let x, y be Nat; :: thesis: for f being FinSequence st f /^ 1 is one-to-one & 1 < x & x <= len f & 1 < y & y <= len f & f . x = f . y holds
x = y
let f be FinSequence; :: thesis: ( f /^ 1 is one-to-one & 1 < x & x <= len f & 1 < y & y <= len f & f . x = f . y implies x = y )
assume B1: ( f /^ 1 is one-to-one & 1 < x & x <= len f & 1 < y & y <= len f & f . x = f . y ) ; :: thesis: x = y
then A68: 1 < len f by XXREAL_0:2;
reconsider xm1 = x - 1, ym1 = y - 1 as Element of NAT by NAT_1:21, B1;
B8: len (f /^ 1) = (len f) - 1 by RFINSEQ:def 1, A68;
B9: x + (- 1) <= (len f) + (- 1) by B1, XREAL_1:6;
1 < xm1 + 1 by B1;
then ( 1 <= xm1 & xm1 <= len (f /^ 1) ) by NAT_1:13, B9, B8;
then B4: xm1 in dom (f /^ 1) by FINSEQ_3:25;
B9a: y + (- 1) <= (len f) + (- 1) by B1, XREAL_1:6;
1 < ym1 + 1 by B1;
then ( 1 <= ym1 & ym1 <= len (f /^ 1) ) by NAT_1:13, B9a, B8;
then B5: ym1 in dom (f /^ 1) by FINSEQ_3:25;
(f /^ 1) . xm1 = f . (xm1 + 1) by RFINSEQ:def 1, B4, A68
.= f . (ym1 + 1) by B1
.= (f /^ 1) . ym1 by RFINSEQ:def 1, B5, A68 ;
then xm1 = ym1 by B1, FUNCT_1:def 4, B4, B5;
hence x = y ; :: thesis: verum