let i, j be 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 that

A1: i in dom f and

A2: j in dom f ; :: thesis: not mid (f,i,j) is empty

len (mid (f,i,j)) >= 1 by A1, A2, Lm8;

hence not mid (f,i,j) is empty ; :: thesis: verum

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 that

A1: i in dom f and

A2: j in dom f ; :: thesis: not mid (f,i,j) is empty

len (mid (f,i,j)) >= 1 by A1, A2, Lm8;

hence not mid (f,i,j) is empty ; :: thesis: verum