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
f ^ CR is_terminated_by CR
let f, CR be FinSequence of D; :: thesis: ( not CR is_substring_of f,1 & CR separates_uniquely implies f ^ CR is_terminated_by CR )
A1: ((len (f ^ CR)) + 1) -' (len CR) = (((len f) + (len CR)) + 1) -' (len CR) by FINSEQ_1:22
.= ((len CR) + ((len f) + 1)) -' (len CR)
.= (len f) + 1 by NAT_D:34 ;
len CR <= (len f) + (len CR) by NAT_1:12;
then A2: len CR <= len (f ^ CR) by FINSEQ_1:22;
assume ( not CR is_substring_of f,1 & CR separates_uniquely ) ; :: thesis: f ^ CR is_terminated_by CR
then instr (1,(f ^ CR),CR) = ((len (f ^ CR)) + 1) -' (len CR) by A1, Th19;
hence f ^ CR is_terminated_by CR by A2, FINSEQ_8:def 12; :: thesis: verum