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

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