for D being non empty set
for f being FinSequence of D holds
( ovlcon (f,f) = f & ovlpart (f,f) = f & ovlldiff (f,f) = {} & ovlrdiff (f,f) = {} )