let r1, r2 be 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)))
let p be nonnegative FinSequence of REAL ; ( 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
; 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; ( 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
; (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
;
verum