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 that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f ; :: thesis: not mid f,i,j is empty
A5: j in dom f by A3, A4, FINSEQ_3:27;
i in dom f by A1, A2, FINSEQ_3:27;
hence not mid f,i,j is empty by A5, SPRECT_2:11; :: thesis: verum