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

now :: thesis: for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g

let i be Element of NAT ; :: thesis: ( n <= i & 0 < i implies mid (f,i,((i -' 1) + (len g))) <> g )
assume that
A2: n <= i and
A3: 0 < i ; :: thesis: mid (f,i,((i -' 1) + (len g))) <> g

now :: thesis: ( ( i <= len f & mid (f,i,((i -' 1) + (len g))) <> g ) or ( i > len f & mid (f,i,((i -' 1) + (len g))) <> g ) )

per cases ( i <= len f or i > len f ) ;

case i <= len f ; :: thesis: mid (f,i,((i -' 1) + (len g))) <> g

hence mid (f,i,((i -' 1) + (len g))) <> g by A1, A2; :: thesis: verum

end;

case A4: i > len f ; :: thesis: mid (f,i,((i -' 1) + (len g))) <> g

now :: thesis: ( ( i <= (i -' 1) + (len g) & mid (f,i,((i -' 1) + (len g))) <> g ) or ( i > (i -' 1) + (len g) & contradiction ) )

per cases ( i <= (i -' 1) + (len g) or i > (i -' 1) + (len g) ) ;

case A5: i <= (i -' 1) + (len g) ; :: thesis: mid (f,i,((i -' 1) + (len g))) <> g

then A6: mid (f,i,((i -' 1) + (len g))) = (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) by FINSEQ_6:def 3;

now :: thesis: ( ( i -' 1 <= len f & len (f /^ (i -' 1)) = 0 ) or ( i -' 1 > len f & len (f /^ (i -' 1)) = 0 ) )

per cases ( i -' 1 <= len f or i -' 1 > len f ) ;

case A7: i -' 1 <= len f ; :: thesis: len (f /^ (i -' 1)) = 0

i >= (len f) + 1 by A4, NAT_1:13;
then A8: i - 1 >= ((len f) + 1) - 1 by XREAL_1:9;
0 + 1 <= i by A3, NAT_1:13;
then i -' 1 = i - 1 by XREAL_0:def 2, XREAL_1:48;
then A9: i -' 1 = len f by A7, A8, XXREAL_0:1;
len (f /^ (i -' 1)) = (len f) - (i -' 1) by A7, RFINSEQ:def 1;
hence len (f /^ (i -' 1)) = 0 by A9; :: thesis: verum

end;

case i -' 1 > len f ; :: thesis: len (f /^ (i -' 1)) = 0

then f /^ (i -' 1) = <*> D by RFINSEQ:def 1;
hence len (f /^ (i -' 1)) = 0 ; :: thesis: verum

end;

end;

end;

then A10: (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) = <*> D by FINSEQ_1:58;

now :: thesis: not mid (f,i,((i -' 1) + (len g))) = g

assume A11: mid (f,i,((i -' 1) + (len g))) = g ; :: thesis: contradiction
a12: 0 + 1 <= i by A3, NAT_1:13;
i - 1 < (i + 1) - 1 by XREAL_1:9, XREAL_1:29;
hence contradiction by A5, A6, A10, A11, a12, XREAL_0:def 2; :: thesis: verum

end;

hence mid (f,i,((i -' 1) + (len g))) <> g ; :: thesis: verum

end;

case A13: i > (i -' 1) + (len g) ; :: thesis: contradiction

now :: thesis: not len g > 0

assume len g > 0 ; :: thesis: contradiction
then len g >= 0 + 1 by NAT_1:13;
then A14: (i -' 1) + (len g) >= (i -' 1) + 1 by XREAL_1:7;
0 + 1 <= i by A3, NAT_1:13;
then i -' 1 = i - 1 by XREAL_0:def 2, XREAL_1:48;
hence contradiction by A13, A14; :: thesis: verum

end;

hence contradiction by A1; :: thesis: verum

end;

end;

end;

hence mid (f,i,((i -' 1) + (len g))) <> g ; :: thesis: verum

end;

end;

end;

hence mid (f,i,((i -' 1) + (len g))) <> g ; :: thesis: verum

end;

hence for i being Element of NAT st n <= i & 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g ; :: thesis: verum