let D be non empty set ; :: thesis: for f, CR being File of D holds addcr f,CR is_preposition_of
let f, CR be File of D; :: thesis: addcr f,CR is_preposition_of
addcr f,CR = ovlcon f,CR by FINSEQ_8:def 11
.= f ^ (CR /^ (len (ovlpart f,CR))) by FINSEQ_8:def 3 ;
hence addcr f,CR is_preposition_of by Th25; :: thesis: verum