let D be non empty set ; 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; 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; ( 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
; 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; verum