:: deftheorem defines Entropy ENTROPY1:def 9 :
for p being FinSequence of REAL holds Entropy p = - (Sum (Infor_FinSeq_of p));