let r1, r2 be Real; :: thesis: for p being nonnegative FinSequence of REAL st r1 >= 0 & r2 >= 0 holds
for i being Element of 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 Element of 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 A1: ( r1 >= 0 & r2 >= 0 ) ; :: thesis: for i being Element of 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 Element of 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 A2: ( i in dom p & 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 A2, FINSEQ_3:31;
hence (Infor_FinSeq_of p) . i = (r1 * r2) * (log 2,(r1 * r2)) by A2, Th47
.= ((r1 * r2) * (log 2,r1)) + ((r1 * r2) * (log 2,r2)) by A1, Th6 ;
:: thesis: verum