for D being non empty set
for f, g being FinSequence of D st ( len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) holds
g is_postposition_of f