let x, y be Nat; 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; ( 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 )
; 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
; verum