let D be set ; 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; 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 ; ( 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
; (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
; verum