for D being non empty set
for f, g being FinSequence of D
for n being Nat st not g is_substring_of f,n holds
for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g