let p be non empty ProbFinS FinSequence of REAL ; :: thesis: for k being Nat st k in dom p holds
(Infor_FinSeq_of p) . k <= 0
let k be Nat; :: thesis: ( k in dom p implies (Infor_FinSeq_of p) . k <= 0 )
assume A1: k in dom p ; :: thesis: (Infor_FinSeq_of p) . k <= 0

per cases ( p . k = 0 or ( p . k > 0 & p . k <= 1 ) ) by A1, MATRPROB:53, MATRPROB:def 5;

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

hence (Infor_FinSeq_of p) . k <= 0 by A1, Th48; :: thesis: verum

end;

suppose A2: ( p . k > 0 & p . k <= 1 ) ; :: thesis: (Infor_FinSeq_of p) . k <= 0

then A3: (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) by A1, Th48;
thus (Infor_FinSeq_of p) . k <= 0 :: thesis: verum

proof

A4: log (2,1) = 0 by POWER:51;

per cases ( p . k < 1 or p . k = 1 ) by A2, XXREAL_0:1;

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

then log (2,(p . k)) < 0 by A2, A4, POWER:57;
hence (Infor_FinSeq_of p) . k <= 0 by A2, A3; :: thesis: verum

end;

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

hence (Infor_FinSeq_of p) . k <= 0 by A3, POWER:51; :: thesis: verum

end;

end;

end;

end;

end;