let D be non empty set ; :: thesis: for f being FinSequence of D st 1 <= len f holds
f is_odd_substring_of f, 0
let f be FinSequence of D; :: thesis: ( 1 <= len f implies f is_odd_substring_of f, 0 )
assume A1: 1 <= len f ; :: thesis: f is_odd_substring_of f, 0

now :: thesis: ( len f > 0 implies ex i being odd Element of NAT st
( 0 <= i & i <= len f & mid (f,i,((i -' 1) + (len f))) = f ) )

assume len f > 0 ; :: thesis: ex i being odd Element of NAT st
( 0 <= i & i <= len f & mid (f,i,((i -' 1) + (len f))) = f )
reconsider i = 1 as odd Element of NAT by POLYFORM:4;
take i = i; :: thesis: ( 0 <= i & i <= len f & mid (f,i,((i -' 1) + (len f))) = f )
thus 0 <= i ; :: thesis: ( i <= len f & mid (f,i,((i -' 1) + (len f))) = f )
thus i <= len f by A1; :: thesis: mid (f,i,((i -' 1) + (len f))) = f
thus mid (f,i,((i -' 1) + (len f))) = mid (f,i,(0 + (len f))) by XREAL_1:232
.= f by A1, FINSEQ_6:120 ; :: thesis: verum

end;

hence f is_odd_substring_of f, 0 ; :: thesis: verum