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