let D be non empty set ; :: thesis: for f, CR being File of D holds
( len (addcr (f,CR)) >= len f & len (addcr (f,CR)) >= len CR )
let f, CR be File of D; :: thesis: ( len (addcr (f,CR)) >= len f & len (addcr (f,CR)) >= len CR )
A1: addcr (f,CR) = ovlcon (f,CR) by FINSEQ_8:def 11;
len (ovlcon (f,CR)) = (len f) + ((len CR) -' (len (ovlpart (f,CR)))) by FINSEQ_8:15;
hence len (addcr (f,CR)) >= len f by A1, NAT_1:12; :: thesis: len (addcr (f,CR)) >= len CR
ovlcon (f,CR) = (f | ((len f) -' (len (ovlpart (f,CR))))) ^ CR by FINSEQ_8:11;
then len (ovlcon (f,CR)) = (len (f | ((len f) -' (len (ovlpart (f,CR)))))) + (len CR) by FINSEQ_1:22;
hence len (addcr (f,CR)) >= len CR by A1, NAT_1:12; :: thesis: verum