:: deftheorem defines ovlldiff FINSEQ_8:def 4 :
for D being non empty set
for f, g being FinSequence of D holds ovlldiff (f,g) = f | ((len f) -' (len (ovlpart (f,g))));