let D be non empty set ; for f1 being FinSequence of D
for i1, i2, j being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
(mid (f1,i1,i2)) . j = f1 . ((i1 -' j) + 1)
let f1 be FinSequence of D; for i1, i2, j being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
(mid (f1,i1,i2)) . j = f1 . ((i1 -' j) + 1)
let i1, i2, j be Nat; ( 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 implies (mid (f1,i1,i2)) . j = f1 . ((i1 -' j) + 1) )
assume that
A1:
1 <= i2
and
A2:
i2 <= i1
and
A3:
i1 <= len f1
and
A4:
1 <= j
and
A5:
j <= (i1 -' i2) + 1
; (mid (f1,i1,i2)) . j = f1 . ((i1 -' j) + 1)
A6:
j <= len (mid (f1,i1,i2))
by A1, A2, A3, A5, Th9;
per cases
( i1 = i2 or i2 < i1 )
by A2, XXREAL_0:1;
suppose A7:
i1 = i2
;
(mid (f1,i1,i2)) . j = f1 . ((i1 -' j) + 1)then A8:
(i1 -' i2) + 1 =
0 + 1
by XREAL_1:232
.=
1
;
then (j + i1) -' 1 =
(1 + i1) -' 1
by A4, A5, XXREAL_0:1
.=
(1 + i1) - 1
by NAT_D:37
.=
(i1 - 1) + 1
.=
(i1 -' 1) + 1
by A1, A7, XREAL_1:233
.=
(i1 -' j) + 1
by A4, A5, A8, XXREAL_0:1
;
hence
(mid (f1,i1,i2)) . j = f1 . ((i1 -' j) + 1)
by A1, A3, A4, A6, A7, FINSEQ_6:118;
verum end; suppose A9:
i2 < i1
;
(mid (f1,i1,i2)) . j = f1 . ((i1 -' j) + 1)A10:
i2 <= len f1
by A2, A3, XXREAL_0:2;
1
<= i1
by A1, A2, XXREAL_0:2;
hence
(mid (f1,i1,i2)) . j = f1 . ((i1 -' j) + 1)
by A1, A3, A4, A6, A9, A10, FINSEQ_6:118;
verum end;