for f being FinSequence ex D being non empty set st f is FinSequence of D