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