let D be set ; for p being FinSequence of D
for i, j, k being Element of NAT st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds
(Del (p,i,j)) . k = p . (((j -' i) + k) + 1)
let p be FinSequence of D; for i, j, k being Element of NAT st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds
(Del (p,i,j)) . k = p . (((j -' i) + k) + 1)
let i, j, k be Element of NAT ; ( i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 implies (Del (p,i,j)) . k = p . (((j -' i) + k) + 1) )
assume that
A1:
i in dom p
and
A2:
j in dom p
and
A3:
i <= j
and
A4:
i <= k
and
A5:
k <= (((len p) - j) + i) - 1
; (Del (p,i,j)) . k = p . (((j -' i) + k) + 1)
A6:
i -' 1 <= i
by NAT_D:35;
i -' 1 <= i
by NAT_D:35;
then
k >= i -' 1
by A4, XXREAL_0:2;
then
k - (i -' 1) >= (i -' 1) - (i -' 1)
by XREAL_1:9;
then A7:
k - (i -' 1) = k -' (i -' 1)
by XREAL_0:def 2;
A8:
1 <= i
by A1, FINSEQ_3:25;
then A9:
(i -' 1) + 1 <= k
by A4, XREAL_1:235;
i - 1 >= 1 - 1
by A8, XREAL_1:9;
then A10:
i -' 1 = i - 1
by XREAL_0:def 2;
j - i >= i - i
by A3, XREAL_1:9;
then A11:
j -' i = j - i
by XREAL_0:def 2;
A12:
j <= len p
by A2, FINSEQ_3:25;
then A13:
len (p /^ j) = (len p) - j
by RFINSEQ:def 1;
k <= ((len p) - j) + (i - 1)
by A5;
then A14:
k - (i -' 1) <= (len p) - j
by A10, XREAL_1:20;
1 <= k - (i -' 1)
by A9, XREAL_1:19;
then A15:
k - (i -' 1) in dom (p /^ j)
by A7, A13, A14, FINSEQ_3:25;
i <= len p
by A1, FINSEQ_3:25;
then
len (p | (i -' 1)) = i -' 1
by A6, FINSEQ_1:59, XXREAL_0:2;
hence (Del (p,i,j)) . k =
(p /^ j) . (k - (i -' 1))
by A9, Th5
.=
p . (j + (k + (1 - i)))
by A12, A10, A15, RFINSEQ:def 1
.=
p . (((j -' i) + k) + 1)
by A11
;
verum