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;
len q = len (Infor_FinSeq_of q) by Th47;
then A3: dom q = dom (Infor_FinSeq_of q) by FINSEQ_3:31;
A4: dom ((r * (log 2,r)) * p) = dom p by VALUED_1:def 5;
A5: len (FinSeq_log 2,p) = len p by Def6;
then A6: dom (FinSeq_log 2,p) = dom p by FINSEQ_3:31;
len (mlt p,(FinSeq_log 2,p)) = len p by A5, MATRPROB:30;
then A7: dom (mlt p,(FinSeq_log 2,p)) = dom p by FINSEQ_3:31;
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 A4, FINSEQ_3:31;
then len (((r * (log 2,r)) * p) + (r * (mlt p,(FinSeq_log 2,p)))) = len ((r * (log 2,r)) * p) by INTEGRA5:2;
then A8: dom (((r * (log 2,r)) * p) + (r * (mlt p,(FinSeq_log 2,p)))) = dom ((r * (log 2,r)) * p) by FINSEQ_3:31;

now

let k be Nat; :: thesis: ( k in dom (Infor_FinSeq_of q) implies (Infor_FinSeq_of q) . b₁ = (((r * (log 2,r)) * p) + (r * (mlt p,(FinSeq_log 2,p)))) . b₁ )
assume A9: k in dom (Infor_FinSeq_of q) ; :: thesis: (Infor_FinSeq_of q) . b₁ = (((r * (log 2,r)) * p) + (r * (mlt p,(FinSeq_log 2,p)))) . b₁
( p . k >= 0 & q . k = r * (p . k) ) by A2, A3, A9, Def1, RVSUM_1:66;
then A10: (Infor_FinSeq_of q) . k = ((r * (p . k)) * (log 2,r)) + ((r * (p . k)) * (log 2,(p . k))) by A1, A3, A9, Th50;
A11: ((r * (log 2,r)) * p) . k = (r * (log 2,r)) * (p . k) by RVSUM_1:66;
A12: (r * (mlt p,(FinSeq_log 2,p))) . k = r * ((mlt p,(FinSeq_log 2,p)) . k) by RVSUM_1:66
.= r * ((p . k) * ((FinSeq_log 2,p) . k)) by A2, A3, A7, A9, RVSUM_1:86
.= (r * (p . k)) * ((FinSeq_log 2,p) . k) ;

per cases ( p . k > 0 or p . k = 0 ) by A2, A3, A9, Def1;

suppose p . k > 0 ; :: thesis: (Infor_FinSeq_of q) . b₁ = (((r * (log 2,r)) * p) + (r * (mlt p,(FinSeq_log 2,p)))) . b₁

then (Infor_FinSeq_of q) . k = (((r * (log 2,r)) * p) . k) + ((r * (mlt p,(FinSeq_log 2,p))) . k) by A2, A3, A6, A9, 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, A3, A4, A8, A9, VALUED_1:def 1; :: thesis: verum

end;

suppose p . k = 0 ; :: thesis: (Infor_FinSeq_of q) . b₁ = (((r * (log 2,r)) * p) + (r * (mlt p,(FinSeq_log 2,p)))) . b₁

hence (Infor_FinSeq_of q) . k = (((r * (log 2,r)) * p) + (r * (mlt p,(FinSeq_log 2,p)))) . k by A2, A3, A4, A8, A9, 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, A3, A4, A8, FINSEQ_1:17; :: thesis: verum