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: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 A3, 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 A6: dom (((r * (log 2,r)) * p) + (r * (mlt p,(FinSeq_log 2,p)))) = dom ((r * (log 2,r)) * p) by FINSEQ_3:31;
len q = len (Infor_FinSeq_of q) by Th47;
then A7: dom q = dom (Infor_FinSeq_of q) by FINSEQ_3:31;
A8: dom (FinSeq_log 2,p) = dom p by A4, 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₁
A10: q . k = r * (p . k) by RVSUM_1:66;
p . k >= 0 by A2, A7, A9, Def1;
then A11: (Infor_FinSeq_of q) . k = ((r * (p . k)) * (log 2,r)) + ((r * (p . k)) * (log 2,(p . k))) by A1, A7, A9, A10, Th50;
A12: ((r * (log 2,r)) * p) . k = (r * (log 2,r)) * (p . k) by RVSUM_1:66;
A13: (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 RVSUM_1:86
.= (r * (p . k)) * ((FinSeq_log 2,p) . k) ;

per cases ( p . k > 0 or p . k = 0 ) by A2, A7, 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, A7, A8, A9, A11, A12, A13, Def6;
hence (Infor_FinSeq_of q) . k = (((r * (log 2,r)) * p) + (r * (mlt p,(FinSeq_log 2,p)))) . k by A2, A7, A3, A6, 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, A7, A3, A6, A9, A11, A12, A13, 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, A7, A3, A6, FINSEQ_1:17; :: thesis: verum