let D be non empty set ; :: thesis: for f, g being FinSequence of D
for n, m being Nat st m >= n holds
( ( g is_odd_substring_of f,m implies g is_odd_substring_of f,n ) & ( g is_even_substring_of f,m implies g is_even_substring_of f,n ) )
let f, g be FinSequence of D; :: thesis: for n, m being Nat st m >= n holds
( ( g is_odd_substring_of f,m implies g is_odd_substring_of f,n ) & ( g is_even_substring_of f,m implies g is_even_substring_of f,n ) )
let n, m be Nat; :: thesis: ( m >= n implies ( ( g is_odd_substring_of f,m implies g is_odd_substring_of f,n ) & ( g is_even_substring_of f,m implies g is_even_substring_of f,n ) ) )
assume A1: m >= n ; :: thesis: ( ( g is_odd_substring_of f,m implies g is_odd_substring_of f,n ) & ( g is_even_substring_of f,m implies g is_even_substring_of f,n ) )

hereby :: thesis: ( g is_even_substring_of f,m implies g is_even_substring_of f,n )

assume A2: g is_odd_substring_of f,m ; :: thesis: g is_odd_substring_of f,n

per cases ( len g > 0 or not len g > 0 ) ;

suppose len g > 0 ; :: thesis: g is_odd_substring_of f,n

then consider i being odd Nat such that
A3: ( m <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) by A2;
n <= i by A1, A3, XXREAL_0:2;
hence g is_odd_substring_of f,n by A3; :: thesis: verum

end;

suppose not len g > 0 ; :: thesis: g is_odd_substring_of f,n

hence g is_odd_substring_of f,n ; :: thesis: verum

end;

end;

end;

assume A4: g is_even_substring_of f,m ; :: thesis: g is_even_substring_of f,n

per cases ( len g > 0 or not len g > 0 ) ;

suppose len g > 0 ; :: thesis: g is_even_substring_of f,n

then consider i being even Nat such that
A5: ( m <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) by A4;
n <= i by A1, A5, XXREAL_0:2;
hence g is_even_substring_of f,n by A5; :: thesis: verum

end;

suppose not len g > 0 ; :: thesis: g is_even_substring_of f,n

hence g is_even_substring_of f,n ; :: thesis: verum

end;

end;