theorem :: FINSEQ_8:14

for D being non empty set
for f, g being FinSequence of D holds
( ovlpart ((f ^ g),g) = g & ovlpart (f,(f ^ g)) = f )