for D being non empty set
for f being non empty one-to-one FinSequence of D holds (f /. (len f)) .. f = len f