:: deftheorem defines is_terminated_by FINSEQ_8:def 12 :
for D being non empty set
for r, CR being FinSequence of D holds
( r is_terminated_by CR iff ( len CR > 0 implies ( len r >= len CR & instr (1,r,CR) = ((len r) + 1) -' (len CR) ) ) );