let D be non empty set ; :: thesis: for f, g being FinSequence of D
for n being Nat holds
( not g is_substring_of f,n or len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )
let f, g be FinSequence of D; :: thesis: for n being Nat holds
( not g is_substring_of f,n or len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )
let n be Nat; :: thesis: ( not g is_substring_of f,n or len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )
assume A1: g is_substring_of f,n ; :: thesis: ( len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )

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

suppose A2: len g > 0 ; :: thesis: ( len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )

then consider i being Nat such that
A3: ( n <= i & i <= len f ) and
A4: mid (f,i,((i -' 1) + (len g))) = g by A1, FINSEQ_8:def 7;
A5: 1 <= (n -' 1) + (len g) by A2, NAT_1:14;
A6: n <= (n -' 1) + (len g)

proof

A7: (n -' 1) + 1 <= (n -' 1) + (len g) by A2, NAT_1:14, XREAL_1:6;

per cases ( n -' 1 >= 1 or n -' 1 < 1 ) ;

suppose n -' 1 >= 1 ; :: thesis: n <= (n -' 1) + (len g)

hence n <= (n -' 1) + (len g) by A7, NAT_D:43; :: thesis: verum

end;

suppose n -' 1 < 1 ; :: thesis: n <= (n -' 1) + (len g)

then A8: n -' 1 = 0 by NAT_1:14;
then n <= 0 + 1 by NAT_D:36;

per cases then ( n = 0 or n = 1 ) by NAT_1:9;

suppose n = 0 ; :: thesis: n <= (n -' 1) + (len g)

hence n <= (n -' 1) + (len g) ; :: thesis: verum

end;

suppose n = 1 ; :: thesis: n <= (n -' 1) + (len g)

hence n <= (n -' 1) + (len g) by A7, A8; :: thesis: verum

end;

end;

end;

end;

end;

A9: (i -' 1) + (len g) <= len f by A3, A4, Th6;
n -' 1 <= i -' 1 by A3, NAT_D:42;
then (n -' 1) + (len g) <= (i -' 1) + (len g) by XREAL_1:6;
hence ( len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) ) by A5, A6, A9, XXREAL_0:2; :: thesis: verum

end;

suppose len g = 0 ; :: thesis: ( len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )

hence ( len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) ) ; :: thesis: verum

end;

end;