let D be non empty set ; :: thesis: for f, g being FinSequence of D
for n, m being Element of NAT st m >= n & g is_substring_of f,m holds
g is_substring_of f,n
let f, g be FinSequence of D; :: thesis: for n, m being Element of NAT st m >= n & g is_substring_of f,m holds
g is_substring_of f,n
let n, m be Element of 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

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

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

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

end;

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

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

end;

end;

end;

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