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,i1,i2)),i) = LSeg (f,((i + i1) -' 1))
let i1, i2, i be 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:233;
then
i + i1 < ((i2 - i1) + 1) + i1
by A5, XREAL_1:6;
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:7;
then
(1 + 1) - 1 <= (i + i1) - 1
by XREAL_1:9;
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 3;
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, Th8;
then A17: (mid (f,i1,i2)) /. i =
(mid (f,i1,i2)) . i
by A4, FINSEQ_4:15
.=
f . ((i + i1) -' 1)
by A1, A2, A3, A4, A5, FINSEQ_6:122
.=
f /. ((i + i1) -' 1)
by A10, A9, FINSEQ_4:15
;
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:15, NAT_1:11
.=
f . (((i + 1) + i1) -' 1)
by A1, A2, A3, A13, A15, FINSEQ_6:122
.=
f /. (((i + 1) + i1) -' 1)
by A11, A14, A6, FINSEQ_4:15
;
hence
LSeg ((mid (f,i1,i2)),i) = LSeg (f,((i + i1) -' 1))
by A4, A18, A12, A6, A17, TOPREAL1:def 3; verum