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