let r1, r2 be Real; :: thesis: for p being nonnegative FinSequence of REAL st r1 >= 0 & r2 >= 0 holds
for i being Nat st i in dom p & p . i = r1 * r2 holds
(Infor_FinSeq_of p) . i = ((r1 * r2) * (log (2,r1))) + ((r1 * r2) * (log (2,r2)))
let p be nonnegative FinSequence of REAL ; :: thesis: ( r1 >= 0 & r2 >= 0 implies for i being Nat st i in dom p & p . i = r1 * r2 holds
(Infor_FinSeq_of p) . i = ((r1 * r2) * (log (2,r1))) + ((r1 * r2) * (log (2,r2))) )
assume that
A1: r1 >= 0 and
A2: r2 >= 0 ; :: thesis: for i being Nat st i in dom p & p . i = r1 * r2 holds
(Infor_FinSeq_of p) . i = ((r1 * r2) * (log (2,r1))) + ((r1 * r2) * (log (2,r2)))
let i be Nat; :: thesis: ( i in dom p & p . i = r1 * r2 implies (Infor_FinSeq_of p) . i = ((r1 * r2) * (log (2,r1))) + ((r1 * r2) * (log (2,r2))) )
assume that
A3: i in dom p and
A4: p . i = r1 * r2 ; :: thesis: (Infor_FinSeq_of p) . i = ((r1 * r2) * (log (2,r1))) + ((r1 * r2) * (log (2,r2)))
len p = len (Infor_FinSeq_of p) by Th47;
then i in dom (Infor_FinSeq_of p) by A3, FINSEQ_3:29;
hence (Infor_FinSeq_of p) . i = (r1 * r2) * (log (2,(r1 * r2))) by A4, Th47
.= ((r1 * r2) * (log (2,r1))) + ((r1 * r2) * (log (2,r2))) by A1, A2, Th6 ;
:: thesis: verum