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:35;
hence len (addcr f,CR) >= len CR by A1, NAT_1:12; :: thesis: verum