let D be set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: (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 ;
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 ;
then A9: (i -' 1) + 1 <= k by ;
i - 1 >= 1 - 1 by ;
then A10: i -' 1 = i - 1 by XREAL_0:def 2;
j - i >= i - i by ;
then A11: j -' i = j - i by XREAL_0:def 2;
A12: j <= len p by ;
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 ;
1 <= k - (i -' 1) by ;
then A15: k - (i -' 1) in dom (p /^ j) by ;
i <= len p by ;
then len (p | (i -' 1)) = i -' 1 by ;
hence (Del (p,i,j)) . k = (p /^ j) . (k - (i -' 1)) by
.= p . (j + (k + (1 - i))) by
.= p . (((j -' i) + k) + 1) by A11 ;
:: thesis: verum