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

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