for D being non empty set
for f, g being FinSequence of D
for n being Nat st g is_odd_substring_of f,n holds
g is_substring_of f,n by FINSEQ_8:def 7;