let D be non empty set ; for f1 being FinSequence of D
for i1, i2, j being Nat st 1 <= i1 & i1 <= i2 & i2 <= len f1 holds
(mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2
let f1 be FinSequence of D; for i1, i2, j being Nat st 1 <= i1 & i1 <= i2 & i2 <= len f1 holds
(mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2
let i1, i2, j be Nat; ( 1 <= i1 & i1 <= i2 & i2 <= len f1 implies (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2 )
assume that
A1:
1 <= i1
and
A2:
i1 <= i2
and
A3:
i2 <= len f1
; (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2
A4:
i1 <= len f1
by A2, A3, XXREAL_0:2;
A5:
1 <= i2
by A1, A2, XXREAL_0:2;
then
len (mid (f1,i1,i2)) = (i2 -' i1) + 1
by A1, A2, A3, A4, FINSEQ_6:118;
then
1 <= len (mid (f1,i1,i2))
by NAT_1:11;
then A6: (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) =
f1 . (((len (mid (f1,i1,i2))) + i1) -' 1)
by A1, A2, A3, A5, A4, FINSEQ_6:118
.=
f1 . ((((i2 -' i1) + 1) + i1) -' 1)
by A1, A2, A3, A5, A4, FINSEQ_6:118
;
((i2 -' i1) + 1) + i1 =
((i2 - i1) + 1) + i1
by A2, XREAL_1:233
.=
i2 + 1
;
hence
(mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2
by A6, NAT_D:34; verum