let D be set ; :: thesis: for p being FinSequence of D

for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds

(Del (p,i,j)) . k = p . k

let p be FinSequence of D; :: thesis: for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds

(Del (p,i,j)) . k = p . k

let i, j, k be Element of NAT ; :: thesis: ( i in dom p & 1 <= k & k <= i - 1 implies (Del (p,i,j)) . k = p . k )

assume that

A1: i in dom p and

A2: 1 <= k and

A3: k <= i - 1 ; :: thesis: (Del (p,i,j)) . k = p . k

A4: i <= len p by A1, FINSEQ_3:25;

A5: k <= i -' 1 by A3, XREAL_0:def 2;

A6: i -' 1 <= i by NAT_D:35;

then len (p | (i -' 1)) = i -' 1 by A4, FINSEQ_1:59, XXREAL_0:2;

then A7: k in dom (p | (i -' 1)) by A2, A5, FINSEQ_3:25;

i -' 1 <= len p by A4, A6, XXREAL_0:2;

then k <= len p by A5, XXREAL_0:2;

then A8: k in dom p by A2, FINSEQ_3:25;

thus (Del (p,i,j)) . k = (p | (i -' 1)) . k by A7, FINSEQ_1:def 7

.= (p | (i -' 1)) /. k by A7, PARTFUN1:def 6

.= p /. k by A7, FINSEQ_4:70

.= p . k by A8, PARTFUN1:def 6 ; :: thesis: verum

for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds

(Del (p,i,j)) . k = p . k

let p be FinSequence of D; :: thesis: for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds

(Del (p,i,j)) . k = p . k

let i, j, k be Element of NAT ; :: thesis: ( i in dom p & 1 <= k & k <= i - 1 implies (Del (p,i,j)) . k = p . k )

assume that

A1: i in dom p and

A2: 1 <= k and

A3: k <= i - 1 ; :: thesis: (Del (p,i,j)) . k = p . k

A4: i <= len p by A1, FINSEQ_3:25;

A5: k <= i -' 1 by A3, XREAL_0:def 2;

A6: i -' 1 <= i by NAT_D:35;

then len (p | (i -' 1)) = i -' 1 by A4, FINSEQ_1:59, XXREAL_0:2;

then A7: k in dom (p | (i -' 1)) by A2, A5, FINSEQ_3:25;

i -' 1 <= len p by A4, A6, XXREAL_0:2;

then k <= len p by A5, XXREAL_0:2;

then A8: k in dom p by A2, FINSEQ_3:25;

thus (Del (p,i,j)) . k = (p | (i -' 1)) . k by A7, FINSEQ_1:def 7

.= (p | (i -' 1)) /. k by A7, PARTFUN1:def 6

.= p /. k by A7, FINSEQ_4:70

.= p . k by A8, PARTFUN1:def 6 ; :: thesis: verum