for D being non empty set
for f, g being FinSequence of D
for n being Element of NAT st g is_substring_of f | n,1 & len g > 0 holds
g is_substring_of f,1