let D be non empty set ; :: thesis: for f, CR being FinSequence of D st not CR is_substring_of f,1 & CR separates_uniquely holds
instr (1,(f ^ CR),CR) = (len f) + 1
let f, CR be FinSequence of D; :: thesis: ( not CR is_substring_of f,1 & CR separates_uniquely implies instr (1,(f ^ CR),CR) = (len f) + 1 )
assume that
A1: not CR is_substring_of f,1 and
A2: CR separates_uniquely ; :: thesis: instr (1,(f ^ CR),CR) = (len f) + 1
A3: len CR > 0 by A1, FINSEQ_8:def 7;
then A4: len CR >= 0 + 1 by NAT_1:13;
A5: for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of (f ^ CR) /^ (j -' 1) holds
j >= (len f) + 1

proof

set i0 = (len f) + 1;
set j0 = (((len f) + 1) + (len CR)) -' 1;
let j be Element of NAT ; :: thesis: ( j >= 1 & j > 0 & CR is_preposition_of (f ^ CR) /^ (j -' 1) implies j >= (len f) + 1 )
assume that
A6: j >= 1 and
j > 0 and
A7: CR is_preposition_of (f ^ CR) /^ (j -' 1) ; :: thesis: j >= (len f) + 1
A8: ( len CR > 0 implies ( 1 <= len ((f ^ CR) /^ (j -' 1)) & mid (((f ^ CR) /^ (j -' 1)),1,(len CR)) = CR ) ) by A7, FINSEQ_8:def 8;
A9: 0 + j < (len CR) + j by A3, XREAL_1:8;
then j + 1 <= (len CR) + j by NAT_1:13;
then A10: j <= ((len CR) + j) - 1 by XREAL_1:19;
1 <= (len CR) + j by A6, A9, XXREAL_0:2;
then A11: ((len CR) + j) - 1 >= 0 by XREAL_1:48;
then A12: ((len CR) + j) -' 1 = ((len CR) + j) - 1 by XREAL_0:def 2;
(len CR) - 1 >= 0 by A4, XREAL_1:48;
then ((((len CR) + j) -' 1) -' j) + 1 = ((((len CR) + j) - 1) - j) + 1 by A12, XREAL_0:def 2
.= len CR ;
then A13: ((f ^ CR) /^ (j -' 1)) | (((((len CR) + j) -' 1) -' j) + 1) = CR by A4, A8, FINSEQ_6:116;
(j + (len CR)) - 1 >= 0 by A6, NAT_1:12, XREAL_1:48;
then A14: (j + (len CR)) -' 1 = (j + (len CR)) - 1 by XREAL_0:def 2;
A15: (((len f) + 1) + (len CR)) -' 1 = (((len f) + (len CR)) + 1) -' 1
.= (len f) + (len CR) by NAT_D:34 ;
(((len f) + 1) + (len CR)) -' 1 = (((len CR) + (len f)) + 1) -' 1
.= (len CR) + (len f) by NAT_D:34 ;
then mid ((f ^ CR),((len f) + 1),((((len f) + 1) + (len CR)) -' 1)) = CR by A4, Th5;
then A16: smid ((f ^ CR),((len f) + 1),((((len f) + 1) + (len CR)) -' 1)) = CR by A4, A15, FINSEQ_8:4, XREAL_1:7;
A17: ( len CR > 0 implies len CR >= 0 + 1 ) by NAT_1:13;
then j + (len CR) >= j + 1 by A1, FINSEQ_8:def 7, XREAL_1:7;
then A18: (j + (len CR)) - 1 >= (j + 1) - 1 by XREAL_1:9;
j + (len CR) >= j + 1 by A1, A17, FINSEQ_8:def 7, XREAL_1:7;
then A19: (j + (len CR)) - 1 >= (j + 1) - 1 by XREAL_1:9;
A20: j - 1 >= 0 by A6, XREAL_1:48;
then A21: j -' 1 = j - 1 by XREAL_0:def 2;
(j -' 1) + (len CR) = (j - 1) + (len CR) by A20, XREAL_0:def 2
.= ((len CR) + j) -' 1 by A11, XREAL_0:def 2 ;
then A22: mid ((f ^ CR),j,((j -' 1) + (len CR))) = CR by A10, A12, A13, FINSEQ_6:def 3;
(j -' 1) + (len CR) = (j - 1) + (len CR) by A20, XREAL_0:def 2
.= (j + (len CR)) - 1 ;
then A23: smid ((f ^ CR),j,((j + (len CR)) -' 1)) = CR by A14, A19, A22, FINSEQ_8:4;

now :: thesis: not j < (len f) + 1

assume A24: j < (len f) + 1 ; :: thesis: contradiction
then ((len f) + 1) - j > 0 by XREAL_1:50;
then A25: ((len f) + 1) -' j = ((len f) + 1) - j by XREAL_0:def 2;
(((len f) + 1) + (len CR)) -' 1 <= len (f ^ CR) by A15, FINSEQ_1:22;
then ((len f) + 1) -' j >= len CR by A2, A6, A16, A23, A24, FINSEQ_8:def 6;
then (((len f) + 1) - j) + j >= (len CR) + j by A25, XREAL_1:7;
then ((len f) + 1) - 1 >= (j + (len CR)) - 1 by XREAL_1:9;
then mid (f,j,((j -' 1) + (len CR))) = CR by A6, A21, A18, A22, Th6;
then j > len f by A1, A6, FINSEQ_8:def 7;
hence contradiction by A24, NAT_1:13; :: thesis: verum

end;

hence j >= (len f) + 1 ; :: thesis: verum

end;

(f ^ CR) /^ (len f) = CR ;
then ( (len f) + 1 <> 0 implies ( 1 <= (len f) + 1 & CR is_preposition_of (f ^ CR) /^ (((len f) + 1) -' 1) & ( for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of (f ^ CR) /^ (j -' 1) holds
j >= (len f) + 1 ) ) ) by A5, NAT_1:11, NAT_D:34;
hence instr (1,(f ^ CR),CR) = (len f) + 1 by FINSEQ_8:def 10; :: thesis: verum