:: deftheorem Def10 defines instr FINSEQ_8:def 10 :
for D being non empty set
for f, g being FinSequence of D
for n being Nat
for b₅ being Element of NAT holds
( b₅ = instr (n,f,g) iff ( ( b₅ <> 0 implies ( n <= b₅ & g is_preposition_of f /^ (b₅ -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds
j >= b₅ ) ) ) & ( b₅ = 0 implies not g is_substring_of f,n ) ) );