for r1, r2 being Real
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)))