theorem Th11: :: FINSEQ_8:11

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