let D be non empty set ; :: thesis: for CR, r being File of D holds addcr r,CR = (ovlldiff r,CR) ^ CR
let CR, r be File of D; :: thesis: addcr r,CR = (ovlldiff r,CR) ^ CR
addcr r,CR = ovlcon r,CR by FINSEQ_8:def 11
.= (ovlldiff r,CR) ^ ((ovlpart r,CR) ^ (ovlrdiff r,CR)) by FINSEQ_8:12
.= (ovlldiff r,CR) ^ CR by Th32 ;
hence addcr r,CR = (ovlldiff r,CR) ^ CR ; :: thesis: verum