theorem Th15: :: FINSEQ_8:15

for D being non empty set
for f, g being FinSequence of D holds
( len (ovlcon (f,g)) = ((len f) + (len g)) - (len (ovlpart (f,g))) & len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) & len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) )