let p be nonnegative FinSequence of REAL ; :: thesis: for q being FinSequence of REAL holds
( q = Infor_FinSeq_of p iff ( len q = len p & ( for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ) ) )
let q be FinSequence of REAL ; :: thesis: ( q = Infor_FinSeq_of p iff ( len q = len p & ( for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ) ) )
set pp = mlt (p,(FinSeq_log (2,p)));
A1: len p = len (FinSeq_log (2,p)) by Def6;
then A2: len (mlt (p,(FinSeq_log (2,p)))) = len p by MATRPROB:30;

hereby :: thesis: ( len q = len p & ( for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ) implies q = Infor_FinSeq_of p )

assume A3: q = Infor_FinSeq_of p ; :: thesis: ( len q = len p & ( for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ) )
thus ( len q = len p & ( for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ) ) :: thesis: verum

proof

A4: dom p = dom q by A2, A3, FINSEQ_3:29;
thus len q = len p by A1, A3, MATRPROB:30; :: thesis: for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(p . k)))
let k be Nat; :: thesis: ( k in dom q implies q . k = (p . k) * (log (2,(p . k))) )
assume A5: k in dom q ; :: thesis: q . k = (p . k) * (log (2,(p . k)))
A6: q . k = (p . k) * ((FinSeq_log (2,p)) . k) by A3, RVSUM_1:59;
A7: k in dom (FinSeq_log (2,p)) by A1, A2, A3, A5, FINSEQ_3:29;

per cases ( p . k = 0 or p . k > 0 ) by A5, A4, Def1;

suppose p . k = 0 ; :: thesis: q . k = (p . k) * (log (2,(p . k)))

hence q . k = (p . k) * (log (2,(p . k))) by A6; :: thesis: verum

end;

suppose p . k > 0 ; :: thesis: q . k = (p . k) * (log (2,(p . k)))

hence q . k = (p . k) * (log (2,(p . k))) by A6, A7, Def6; :: thesis: verum

end;

end;

end;

end;

assume that
A8: len q = len p and
A9: for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ; :: thesis: q = Infor_FinSeq_of p
A10: dom q = dom p by A8, FINSEQ_3:29;
len q = len (mlt (p,(FinSeq_log (2,p)))) by A1, A8, MATRPROB:30;
then A11: dom q = dom (mlt (p,(FinSeq_log (2,p)))) by FINSEQ_3:29;
A12: dom p = dom (FinSeq_log (2,p)) by A1, FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom q holds
q . k = (mlt (p,(FinSeq_log (2,p)))) . k

let k be Nat; :: thesis: ( k in dom q implies q . b₁ = (mlt (p,(FinSeq_log (2,p)))) . b₁ )
assume A13: k in dom q ; :: thesis: q . b₁ = (mlt (p,(FinSeq_log (2,p)))) . b₁
A14: (mlt (p,(FinSeq_log (2,p)))) . k = (p . k) * ((FinSeq_log (2,p)) . k) by RVSUM_1:59;

per cases ( p . k = 0 or p . k > 0 ) by A10, A13, Def1;

suppose A15: p . k = 0 ; :: thesis: q . b₁ = (mlt (p,(FinSeq_log (2,p)))) . b₁

hence q . k = 0 * (log (2,(p . k))) by A9, A13
.= (mlt (p,(FinSeq_log (2,p)))) . k by A14, A15 ;
:: thesis: verum

end;

suppose p . k > 0 ; :: thesis: (mlt (p,(FinSeq_log (2,p)))) . b₁ = q . b₁

then (FinSeq_log (2,p)) . k = log (2,(p . k)) by A12, A10, A13, Def6;
hence (mlt (p,(FinSeq_log (2,p)))) . k = (p . k) * (log (2,(p . k))) by RVSUM_1:59
.= q . k by A9, A13 ;
:: thesis: verum

end;

end;

end;

hence q = Infor_FinSeq_of p by A11, FINSEQ_1:13; :: thesis: verum