let p be non empty ProbFinS FinSequence of REAL ; :: thesis: Entropy p >= 0
set p1 = - (Infor_FinSeq_of p);
A1: dom p = Seg (len p) by FINSEQ_1:def 3
.= Seg (len (Infor_FinSeq_of p)) by Th47
.= dom (Infor_FinSeq_of p) by FINSEQ_1:def 3 ;
A2: for k being Nat st k in dom (- (Infor_FinSeq_of p)) holds
(- (Infor_FinSeq_of p)) . k >= 0

proof

let k be Nat; :: thesis: ( k in dom (- (Infor_FinSeq_of p)) implies (- (Infor_FinSeq_of p)) . k >= 0 )
assume k in dom (- (Infor_FinSeq_of p)) ; :: thesis: (- (Infor_FinSeq_of p)) . k >= 0
then k in dom p by A1, VALUED_1:8;
then (Infor_FinSeq_of p) . k <= 0 by Th52;
then - ((Infor_FinSeq_of p) . k) >= - 0 ;
hence (- (Infor_FinSeq_of p)) . k >= 0 by RVSUM_1:17; :: thesis: verum

end;

Entropy p = Sum (- (Infor_FinSeq_of p)) by RVSUM_1:88;
hence Entropy p >= 0 by A2, RVSUM_1:84; :: thesis: verum