let D be set ; for p being FinSequence of D
for i, j being Element of NAT st i in dom p & j in dom p holds
len (Del (p,i,j)) = (((len p) - j) + i) - 1
let p be FinSequence of D; for i, j being Element of NAT st i in dom p & j in dom p holds
len (Del (p,i,j)) = (((len p) - j) + i) - 1
let i, j be Element of NAT ; ( i in dom p & j in dom p implies len (Del (p,i,j)) = (((len p) - j) + i) - 1 )
assume that
A1:
i in dom p
and
A2:
j in dom p
; len (Del (p,i,j)) = (((len p) - j) + i) - 1
A3:
i <= len p
by A1, FINSEQ_3:25;
1 <= i
by A1, FINSEQ_3:25;
then A4:
i - 1 >= 1 - 1
by XREAL_1:9;
A5:
i -' 1 <= i
by NAT_D:35;
A6:
j <= len p
by A2, FINSEQ_3:25;
thus len (Del (p,i,j)) =
(len (p | (i -' 1))) + (len (p /^ j))
by FINSEQ_1:22
.=
(i -' 1) + (len (p /^ j))
by A3, A5, FINSEQ_1:59, XXREAL_0:2
.=
(i -' 1) + ((len p) - j)
by A6, RFINSEQ:def 1
.=
(i - 1) + ((len p) - j)
by A4, XREAL_0:def 2
.=
(((len p) - j) + i) - 1
; verum