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 A2: ( n <= i & 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 A3: 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 A4: i <= (i -' 1) + (len g) ; :: thesis: mid f,i,((i -' 1) + (len g)) <> g

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

A6: now

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

end;

end;

end;

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

now

assume A11: mid f,i,((i -' 1) + (len g)) = g ; :: thesis: contradiction
0 + 1 <= i by A2, NAT_1:13;
then A12: 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 A4, 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

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:9;
0 + 1 <= i by A2, NAT_1:13;
then 0 <= i - 1 by XREAL_1:50;
then i -' 1 = i - 1 by XREAL_0:def 2;
hence contradiction by A13, A14; :: 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