let i, j be Element of NAT ; :: thesis: for D being non empty set
for f being FinSequence of D st i in dom f & j in dom f holds
not mid f,i,j is empty
let D be non empty set ; :: thesis: for f being FinSequence of D st i in dom f & j in dom f holds
not mid f,i,j is empty
let f be FinSequence of D; :: thesis: ( i in dom f & j in dom f implies not mid f,i,j is empty )
assume ( i in dom f & j in dom f ) ; :: thesis: not mid f,i,j is empty
then len (mid f,i,j) >= 1 by Th9;
hence not mid f,i,j is empty by FINSEQ_3:27, RELAT_1:60; :: thesis: verum