for D being non empty set
for f, g being FinSequence of D
for n being Nat holds
( not g is_substring_of f,n or len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )