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