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 Element of 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 Element of 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: dom p = dom (FinSeq_log 2,p) by FINSEQ_3:31;
A3: len (mlt p,(FinSeq_log 2,p)) = len p by A1, MATRPROB:30;

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

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

proof

thus len q = len p by A1, A4, MATRPROB:30; :: thesis: for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log 2,(p . k))
let k be Element of 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: ( dom q = dom (mlt p,(FinSeq_log 2,p)) & dom p = dom q ) by A3, A4, FINSEQ_3:31;
A7: q . k = (p . k) * ((FinSeq_log 2,p) . k) by A4, A5, RVSUM_1:86;
A8: k in dom (FinSeq_log 2,p) by A1, A3, A4, A5, FINSEQ_3:31;

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

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

hence q . k = (p . k) * (log 2,(p . k)) by A7; :: 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 A7, A8, Def6; :: thesis: verum

end;

end;

end;

end;

assume A9: ( len q = len p & ( for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log 2,(p . k)) ) ) ; :: thesis: q = Infor_FinSeq_of p
then len q = len (mlt p,(FinSeq_log 2,p)) by A1, MATRPROB:30;
then A10: ( dom q = dom (mlt p,(FinSeq_log 2,p)) & dom q = dom p ) by A9, FINSEQ_3:31;

now

let k be Nat; :: thesis: ( k in dom q implies q . b₁ = (mlt p,(FinSeq_log 2,p)) . b₁ )
assume A11: k in dom q ; :: thesis: q . b₁ = (mlt p,(FinSeq_log 2,p)) . b₁
A12: (mlt p,(FinSeq_log 2,p)) . k = (p . k) * ((FinSeq_log 2,p) . k) by A10, A11, RVSUM_1:86;

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

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

hence q . k = 0 * (log 2,(p . k)) by A9, A11
.= (mlt p,(FinSeq_log 2,p)) . k by A12, A13 ;
:: 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 A2, A10, A11, Def6;
hence (mlt p,(FinSeq_log 2,p)) . k = (p . k) * (log 2,(p . k)) by A10, A11, RVSUM_1:86
.= q . k by A9, A11 ;
:: thesis: verum

end;

end;

end;

hence q = Infor_FinSeq_of p by A10, FINSEQ_1:17; :: thesis: verum