let D be non empty set ; 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; ( 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; 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; verum