let p be non empty ProbFinS FinSequence of REAL ; :: thesis: ( ex k being Element of NAT st
( k in dom p & p . k = 1 ) implies Entropy p = 0 )
assume A1: ex k being Element of NAT st
( k in dom p & p . k = 1 ) ; :: thesis: Entropy p = 0
consider k1 being Element of NAT such that
A2: ( k1 in dom p & p . k1 = 1 ) by A1;
A3: p has_onlyone_value_in k1 by A2, Th15;
set q = Infor_FinSeq_of p;
len (Infor_FinSeq_of p) = len p by Th47;
then A4: dom (Infor_FinSeq_of p) = dom p by FINSEQ_3:31;
for k being Element of NAT st k in dom (Infor_FinSeq_of p) holds
(Infor_FinSeq_of p) . k = 0

proof

let k be Element of NAT ; :: thesis: ( k in dom (Infor_FinSeq_of p) implies (Infor_FinSeq_of p) . k = 0 )
assume A5: k in dom (Infor_FinSeq_of p) ; :: thesis: (Infor_FinSeq_of p) . k = 0

per cases ( k = k1 or k <> k1 ) ;

suppose k = k1 ; :: thesis: (Infor_FinSeq_of p) . k = 0

hence (Infor_FinSeq_of p) . k = 1 * (log 2,1) by A2, A5, Th47
.= 0 by POWER:59 ;
:: thesis: verum

end;

suppose k <> k1 ; :: thesis: (Infor_FinSeq_of p) . k = 0

then A6: p . k = 0 by A3, A4, A5, Def2;
thus (Infor_FinSeq_of p) . k = (p . k) * (log 2,(p . k)) by A5, Th47
.= 0 by A6 ; :: thesis: verum

end;

end;

end;

then for x being set st x in dom (Infor_FinSeq_of p) holds
(Infor_FinSeq_of p) . x = 0 ;
then Infor_FinSeq_of p = (dom (Infor_FinSeq_of p)) --> 0 by FUNCOP_1:17;
then Infor_FinSeq_of p = (len (Infor_FinSeq_of p)) |-> 0 by FINSEQ_1:def 3;
then Sum (Infor_FinSeq_of p) = 0 by RVSUM_1:111;
hence Entropy p = 0 ; :: thesis: verum