let p be nonnegative FinSequence of REAL ; :: thesis: for k being Nat st k in dom p holds
( ( p . k = 0 implies (Infor_FinSeq_of p) . k = 0 ) & ( p . k > 0 implies (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) ) )
A1: dom p = Seg (len p) by FINSEQ_1:def 3
.= Seg (len (Infor_FinSeq_of p)) by Th47
.= dom (Infor_FinSeq_of p) by FINSEQ_1:def 3 ;
let k be Nat; :: thesis: ( k in dom p implies ( ( p . k = 0 implies (Infor_FinSeq_of p) . k = 0 ) & ( p . k > 0 implies (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) ) ) )
assume A2: k in dom p ; :: thesis: ( ( p . k = 0 implies (Infor_FinSeq_of p) . k = 0 ) & ( p . k > 0 implies (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) ) )

hereby :: thesis: ( p . k > 0 implies (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) )

assume p . k = 0 ; :: thesis: (Infor_FinSeq_of p) . k = 0
hence (Infor_FinSeq_of p) . k = 0 * (log (2,(p . k))) by A2, A1, Th47
.= 0 ;
:: thesis: verum

end;

thus ( p . k > 0 implies (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) ) by A2, A1, Th47; :: thesis: verum