for D being set holds D * is FinSequenceSet of D