let p be nonnegative FinSequence of REAL ; :: thesis: for k being Element of 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)) ) )
let k be Element of 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 A1: 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)) ) )
A2: 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 ;

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 A1, A2, Th47
.= 0 ;
:: thesis: verum

end;

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