let f be FinSequence of (TOP-REAL 2); for i1, i2, i being Element of NAT st 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 holds
LSeg (mid f,i1,i2),i = LSeg f,((i + i1) -' 1)
let i1, i2, i be Element of NAT ; ( 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 implies LSeg (mid f,i1,i2),i = LSeg f,((i + i1) -' 1) )
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,i1,i2),i = LSeg f,((i + i1) -' 1)
A6: ((i + i1) -' 1) + 1 =
((i + i1) - 1) + 1
by A1, NAT_D:37
.=
((i + 1) + i1) - 1
.=
((i + 1) + i1) -' 1
by A1, NAT_D:37
;
(i2 - i1) + 1 = (i2 -' i1) + 1
by A2, XREAL_1:235;
then
i + i1 < ((i2 - i1) + 1) + i1
by A5, XREAL_1:8;
then
((i + i1) + 1) - 1 <= (i2 + 1) - 1
by NAT_1:13;
then A7:
((i + i1) - 1) + 1 <= len f
by A3, XXREAL_0:2;
then A8:
((i + i1) -' 1) + 1 <= len f
by A1, NAT_D:37;
then A9:
(i + i1) -' 1 < len f
by NAT_1:13;
1 + 1 <= i + i1
by A1, A4, XREAL_1:9;
then
(1 + 1) - 1 <= (i + i1) - 1
by XREAL_1:11;
then A10:
1 <= (i + i1) -' 1
by A1, NAT_D:37;
then A11:
1 < ((i + i1) -' 1) + 1
by NAT_1:13;
A12:
LSeg f,((i + i1) -' 1) = LSeg (f /. ((i + i1) -' 1)),(f /. (((i + i1) -' 1) + 1))
by A10, A8, TOPREAL1:def 5;
A13:
i + 1 <= (i2 -' i1) + 1
by A5, NAT_1:13;
A14:
((i + i1) -' 1) + 1 <= len f
by A1, A7, NAT_D:37;
A15:
1 <= 1 + i
by NAT_1:11;
A16:
i < len (mid f,i1,i2)
by A1, A2, A3, A5, Th20;
then A17: (mid f,i1,i2) /. i =
(mid f,i1,i2) . i
by A4, FINSEQ_4:24
.=
f . ((i + i1) -' 1)
by A1, A2, A3, A4, A5, FINSEQ_6:128
.=
f /. ((i + i1) -' 1)
by A10, A9, FINSEQ_4:24
;
A18:
i + 1 <= len (mid f,i1,i2)
by A16, NAT_1:13;
i + 1 <= len (mid f,i1,i2)
by A16, NAT_1:13;
then (mid f,i1,i2) /. (i + 1) =
(mid f,i1,i2) . (i + 1)
by FINSEQ_4:24, NAT_1:11
.=
f . (((i + 1) + i1) -' 1)
by A1, A2, A3, A13, A15, FINSEQ_6:128
.=
f /. (((i + 1) + i1) -' 1)
by A11, A14, A6, FINSEQ_4:24
;
hence
LSeg (mid f,i1,i2),i = LSeg f,((i + i1) -' 1)
by A4, A18, A12, A6, A17, TOPREAL1:def 5; verum