for p being non empty ProbFinS FinSequence of REAL holds Entropy p >= 0