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 A1: ( i in dom p & j in dom p ) ; :: thesis: len (Del p,i,j) = (((len p) - j) + i) - 1
then A2: ( 1 <= i & i <= len p ) by FINSEQ_3:27;
then A3: i - 1 >= 1 - 1 by XREAL_1:11;
A4: i -' 1 <= i by NAT_D:35;
A5: j <= len p by A1, FINSEQ_3:27;
thus len (Del p,i,j) = (len (p | (i -' 1))) + (len (p /^ j)) by FINSEQ_1:35
.= (i -' 1) + (len (p /^ j)) by A2, A4, FINSEQ_1:80, XXREAL_0:2
.= (i -' 1) + ((len p) - j) by A5, RFINSEQ:def 2
.= (i - 1) + ((len p) - j) by A3, XREAL_0:def 2
.= (((len p) - j) + i) - 1 ; :: thesis: verum