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