let D be non empty set ; :: thesis: for f, g being FinSequence of D
for n being Element of 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 Element of 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 Element of 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

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

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, Def7; :: thesis: verum

end;

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

now

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 JORDAN3:def 1;

A7: now

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

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

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

end;

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

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

end;

end;

end;

then f /^ (i -' 1) = <*> D ;
then A11: (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) = <*> D by A7, FINSEQ_1:79;

now

assume A12: mid f,i,((i -' 1) + (len g)) = g ; :: thesis: contradiction
0 + 1 <= i by A3, NAT_1:13;
then A13: 0 <= i - 1 by XREAL_1:50;
i < i + 1 by XREAL_1:31;
then i - 1 < (i + 1) - 1 by XREAL_1:11;
hence contradiction by A5, A6, A7, A11, A12, A13, XREAL_0:def 2; :: thesis: verum

end;

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

end;

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

now

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

end;

hence contradiction by A1, Def7; :: 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