theorem Th16: :: GLIB_006:12

for D being non empty set
for f, g being FinSequence of D
for n being even Element of NAT st g is_odd_substring_of f,n holds
g is_odd_substring_of f,n + 1 by Th1;