let f be FinSequence of (TOP-REAL 2); for i1, i2, i being Nat st 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 holds
LSeg ((mid (f,i2,i1)),i) = LSeg (f,(i2 -' i))
let i1, i2, i be Nat; ( 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 implies LSeg ((mid (f,i2,i1)),i) = LSeg (f,(i2 -' i)) )
assume that
A1:
1 <= i1
and
A2:
i1 < i2
and
A3:
i2 <= len f
and
A4:
1 <= i
and
A5:
i < (i2 -' i1) + 1
; LSeg ((mid (f,i2,i1)),i) = LSeg (f,(i2 -' i))
A6:
len (mid (f,i2,i1)) = (i2 -' i1) + 1
by A1, A2, A3, Th9;
i < len (mid (f,i2,i1))
by A1, A2, A3, A5, Th9;
then
i + 1 <= len (mid (f,i2,i1))
by NAT_1:13;
then A7:
(i + 1) - i <= (len (mid (f,i2,i1))) - i
by XREAL_1:9;
then A8:
1 <= (len (mid (f,i2,i1))) -' i
by NAT_D:39;
i2 <= i2 + (i1 -' 1)
by NAT_1:11;
then
i2 <= i2 + (i1 - 1)
by A1, XREAL_1:233;
then
i2 - (i1 - 1) <= (i2 + (i1 - 1)) - (i1 - 1)
by XREAL_1:9;
then
(i2 - i1) + 1 <= i2
;
then A9:
(i2 -' i1) + 1 <= i2
by A2, XREAL_1:233;
A10: ((((i2 -' i1) + 1) -' i) + i1) -' 1 =
((((i2 -' i1) + 1) -' i) + i1) - 1
by A1, NAT_D:37
.=
((((i2 -' i1) + 1) - i) + i1) - 1
by A5, XREAL_1:233
.=
((i2 -' i1) - i) + i1
.=
((i2 - i1) - i) + i1
by A2, XREAL_1:233
.=
i2 - i
.=
i2 -' i
by A5, A9, XREAL_1:233, XXREAL_0:2
;
(len (mid (f,i2,i1))) + 1 <= (len (mid (f,i2,i1))) + i
by A4, XREAL_1:6;
then
len (mid (f,i2,i1)) < (len (mid (f,i2,i1))) + i
by NAT_1:13;
then
(len (mid (f,i2,i1))) - i < ((len (mid (f,i2,i1))) + i) - i
by XREAL_1:9;
then A11:
(len (mid (f,i2,i1))) -' i < (i2 -' i1) + 1
by A6, A7, NAT_D:39;
i + ((len (mid (f,i2,i1))) -' i) = len (mid (f,i2,i1))
by A5, A6, XREAL_1:235;
hence LSeg ((mid (f,i2,i1)),i) =
LSeg ((Rev (mid (f,i2,i1))),((len (mid (f,i2,i1))) -' i))
by SPPOL_2:2
.=
LSeg ((mid (f,i1,i2)),((len (mid (f,i2,i1))) -' i))
by Th18
.=
LSeg (f,((((len (mid (f,i2,i1))) -' i) + i1) -' 1))
by A1, A2, A3, A8, A11, Th19
.=
LSeg (f,(i2 -' i))
by A1, A2, A3, A10, Th9
;
verum