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 i in dom f ; :: thesis: ( not j in dom f or len (mid (f,i,j)) >= 1 )
then A2: ( 1 <= i & i <= len f ) by FINSEQ_3:25;
assume j in dom f ; :: thesis: len (mid (f,i,j)) >= 1
then ( 1 <= j & j <= len f ) by FINSEQ_3:25;
then ( len (mid (f,i,j)) = (i -' j) + 1 or len (mid (f,i,j)) = (j -' i) + 1 ) by A2, A1, FINSEQ_6:118;
hence len (mid (f,i,j)) >= 1 by NAT_1:11; :: thesis: verum