:: deftheorem defines is_even_substring_of GLIB_006:def 2 :
for D being non empty set
for f, g being FinSequence of D
for n being Nat holds
( g is_even_substring_of f,n iff ( len g > 0 implies ex i being even Nat st
( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ) );