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 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 ;

:: thesis: verum

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 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 ;

:: thesis: verum