let f, g be FinSequence; :: thesis: for n, m being Nat st m >= n & g is_substring_of f,m holds
g is_substring_of f,n
let n, m be Nat; :: thesis: ( m >= n & g is_substring_of f,m implies g is_substring_of f,n )
assume that
A1: m >= n and
A2: g is_substring_of f,m ; :: thesis: g is_substring_of f,n

now :: thesis: ( ( len g > 0 & g is_substring_of f,n ) or ( len g <= 0 & g is_substring_of f,n ) )

per cases ( len g > 0 or len g <= 0 ) ;

case len g > 0 ; :: thesis: g is_substring_of f,n

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

end;

case len g <= 0 ; :: thesis: g is_substring_of f,n

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

end;

end;

end;

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