let D be non empty set ; :: thesis: for f, g being FinSequence of D st g is_odd_substring_of f, 0 holds
g is_odd_substring_of f,1
let f, g be FinSequence of D; :: thesis: ( g is_odd_substring_of f, 0 implies g is_odd_substring_of f,1 )
reconsider n = 0 as even Element of NAT ;
assume g is_odd_substring_of f, 0 ; :: thesis: g is_odd_substring_of f,1
then g is_odd_substring_of f,n + 1 by Th16;
hence g is_odd_substring_of f,1 ; :: thesis: verum