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 & len (Del (p,i,j)) = 0 holds
( i = 1 & j = len p )
let p be FinSequence of D; :: thesis: for i, j being Element of NAT st i in dom p & j in dom p & len (Del (p,i,j)) = 0 holds
( i = 1 & j = len p )
let i, j be Element of NAT ; :: thesis: ( i in dom p & j in dom p & len (Del (p,i,j)) = 0 implies ( i = 1 & j = len p ) )
assume that
A1: i in dom p and
A2: j in dom p and
A3: len (Del (p,i,j)) = 0 ; :: thesis: ( i = 1 & j = len p )
A4: 1 <= i by A1, FINSEQ_3:25;
j <= len p by A2, FINSEQ_3:25;
then A5: (len p) - j >= 0 by XREAL_1:48;
A6: (((len p) - j) + i) - 1 = 0 by A1, A2, A3, Th2;
then (len p) - j = 1 - i ;
then 1 >= i by A5, XREAL_1:49;
hence i = 1 by A4, XXREAL_0:1; :: thesis: j = len p
hence j = len p by A6; :: thesis: verum