theorem Th20: :: FINSEQ_8:20

for f, g being FinSequence st g is_substring_of f, 0 holds
g is_substring_of f,1