let D be non empty set ; :: thesis: for f, CR being File of D holds CR is_substring_of addcr f,CR,1
let f, CR be File of D; :: thesis: CR is_substring_of addcr f,CR,1
addcr f,CR = ovlcon f,CR by FINSEQ_8:def 11;
hence CR is_substring_of addcr f,CR,1 by Th40; :: thesis: verum