:: deftheorem Def2 defines ovlpart FINSEQ_8:def 2 :
for D being non empty set
for f, g, b₄ being FinSequence of D holds
( b₄ = ovlpart (f,g) iff ( len b₄ <= len g & b₄ = smid (g,1,(len b₄)) & b₄ = smid (f,(((len f) -' (len b₄)) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds
j <= len b₄ ) ) );