for D being non empty set
for f being FinSequence of D holds f is_terminated_by f