:: deftheorem defines is_substring_of FINSEQ_8:def 7 :
for D being non empty set
for f, g being FinSequence of D
for n being Element of NAT holds
( g is_substring_of f,n iff ( len g > 0 implies ex i being Element of NAT st
( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ) );