let r be Real; :: thesis: for p being nonnegative FinSequence of REAL st r >= 0 holds
Infor_FinSeq_of (r * p) = ((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))
let p be nonnegative FinSequence of REAL ; :: thesis: ( r >= 0 implies Infor_FinSeq_of (r * p) = ((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p))))) )
assume A1: r >= 0 ; :: thesis: Infor_FinSeq_of (r * p) = ((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))
reconsider q = r * p as nonnegative FinSequence of REAL by A1, Th10;
set qq = Infor_FinSeq_of q;
A2: dom q = dom p by VALUED_1:def 5;
A3: dom ((r * (log (2,r))) * p) = dom p by VALUED_1:def 5;
A4: len (FinSeq_log (2,p)) = len p by Def6;
then len (mlt (p,(FinSeq_log (2,p)))) = len p by MATRPROB:30;
then dom (mlt (p,(FinSeq_log (2,p)))) = dom p by FINSEQ_3:29;
then dom (r * (mlt (p,(FinSeq_log (2,p))))) = dom p by VALUED_1:def 5;
then len ((r * (log (2,r))) * p) = len (r * (mlt (p,(FinSeq_log (2,p))))) by A3, FINSEQ_3:29;
then len (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) = len ((r * (log (2,r))) * p) by INTEGRA5:2;
then A5: dom (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) = dom ((r * (log (2,r))) * p) by FINSEQ_3:29;
len q = len (Infor_FinSeq_of q) by Th47;
then A6: dom q = dom (Infor_FinSeq_of q) by FINSEQ_3:29;
A7: dom (FinSeq_log (2,p)) = dom p by A4, FINSEQ_3:29;
now :: thesis: for k being Nat st k in dom (Infor_FinSeq_of q) holds
(Infor_FinSeq_of q) . k = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . k
let k be Nat; :: thesis: ( k in dom (Infor_FinSeq_of q) implies (Infor_FinSeq_of q) . b1 = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . b1 )
assume A8: k in dom (Infor_FinSeq_of q) ; :: thesis: (Infor_FinSeq_of q) . b1 = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . b1
A9: q . k = r * (p . k) by RVSUM_1:44;
p . k >= 0 by A2, A6, A8, Def1;
then A10: (Infor_FinSeq_of q) . k = ((r * (p . k)) * (log (2,r))) + ((r * (p . k)) * (log (2,(p . k)))) by A1, A6, A8, A9, Th50;
A11: ((r * (log (2,r))) * p) . k = (r * (log (2,r))) * (p . k) by RVSUM_1:44;
A12: (r * (mlt (p,(FinSeq_log (2,p))))) . k = r * ((mlt (p,(FinSeq_log (2,p)))) . k) by RVSUM_1:44
.= r * ((p . k) * ((FinSeq_log (2,p)) . k)) by RVSUM_1:59
.= (r * (p . k)) * ((FinSeq_log (2,p)) . k) ;
per cases ( p . k > 0 or p . k = 0 ) by A2, A6, A8, Def1;
suppose p . k > 0 ; :: thesis: (Infor_FinSeq_of q) . b1 = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . b1
then (Infor_FinSeq_of q) . k = (((r * (log (2,r))) * p) . k) + ((r * (mlt (p,(FinSeq_log (2,p))))) . k) by A2, A6, A7, A8, A10, A11, A12, Def6;
hence (Infor_FinSeq_of q) . k = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . k by A2, A6, A3, A5, A8, VALUED_1:def 1; :: thesis: verum
end;
suppose p . k = 0 ; :: thesis: (Infor_FinSeq_of q) . b1 = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . b1
hence (Infor_FinSeq_of q) . k = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . k by A2, A6, A3, A5, A8, A10, A11, A12, VALUED_1:def 1; :: thesis: verum
end;
end;
end;
hence Infor_FinSeq_of (r * p) = ((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p))))) by A2, A6, A3, A5, FINSEQ_1:13; :: thesis: verum