let f be FinSequence of (TOP-REAL 2); for i, n being Nat st n <= len f & 1 <= i holds
LSeg ((f /^ n),i) = LSeg (f,(n + i))
let i, n be Nat; ( n <= len f & 1 <= i implies LSeg ((f /^ n),i) = LSeg (f,(n + i)) )
assume that
A1:
n <= len f
and
A2:
1 <= i
; LSeg ((f /^ n),i) = LSeg (f,(n + i))
per cases
( i + 1 <= (len f) - n or i + 1 > (len f) - n )
;
suppose A3:
i + 1
<= (len f) - n
;
LSeg ((f /^ n),i) = LSeg (f,(n + i))
1
<= i + 1
by NAT_1:11;
then
1
<= (len f) - n
by A3, XXREAL_0:2;
then A4:
1
+ n <= len f
by XREAL_1:19;
n <= 1
+ n
by NAT_1:11;
then
n <= len f
by A4, XXREAL_0:2;
then A5:
len (f /^ n) = (len f) - n
by RFINSEQ:def 1;
then A6:
i in dom (f /^ n)
by A2, A3, SEQ_4:134;
A7:
(i + 1) + n <= len f
by A3, XREAL_1:19;
i <= i + n
by NAT_1:11;
then A8:
1
<= i + n
by A2, XXREAL_0:2;
A9:
i + 1
in dom (f /^ n)
by A2, A3, A5, SEQ_4:134;
thus LSeg (
(f /^ n),
i) =
LSeg (
((f /^ n) /. i),
((f /^ n) /. (i + 1)))
by A2, A3, A5, TOPREAL1:def 3
.=
LSeg (
(f /. (i + n)),
((f /^ n) /. (i + 1)))
by A6, FINSEQ_5:27
.=
LSeg (
(f /. (i + n)),
(f /. ((i + 1) + n)))
by A9, FINSEQ_5:27
.=
LSeg (
(f /. (i + n)),
(f /. ((i + n) + 1)))
.=
LSeg (
f,
(n + i))
by A8, A7, TOPREAL1:def 3
;
verum end; end;