let i, j be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st i in dom f & j in dom f holds
len (mid (f,i,j)) >= 1
let D be non empty set ; :: thesis: for f being FinSequence of D st i in dom f & j in dom f holds
len (mid (f,i,j)) >= 1
let f be FinSequence of D; :: thesis: ( i in dom f & j in dom f implies len (mid (f,i,j)) >= 1 )
A1: ( i <= j or j < i ) ;
assume A2: i in dom f ; :: thesis: ( not j in dom f or len (mid (f,i,j)) >= 1 )
then A3: i <= len f by FINSEQ_3:25;
assume A4: j in dom f ; :: thesis: len (mid (f,i,j)) >= 1
then A5: 1 <= j by FINSEQ_3:25;
A6: j <= len f by A4, FINSEQ_3:25;
1 <= i by A2, FINSEQ_3:25;
then ( len (mid (f,i,j)) = (i -' j) + 1 or len (mid (f,i,j)) = (j -' i) + 1 ) by A3, A5, A6, A1, FINSEQ_6:118;
hence len (mid (f,i,j)) >= 1 by NAT_1:11; :: thesis: verum