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

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