let D be non empty set ; :: thesis: for f being FinSequence of D
for i, j being 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 Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
not mid (f,i,j) is empty
let i, j be 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:25;
i in dom f by A1, A2, FINSEQ_3:25;
hence not mid (f,i,j) is empty by A5, SPRECT_2:7; :: thesis: verum