:: deftheorem defines Infor_FinSeq_of ENTROPY1:def 7 :
for p being FinSequence of REAL holds Infor_FinSeq_of p = mlt (p,(FinSeq_log (2,p)));