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: len (mlt p,(FinSeq_log 2,p)) = len p by 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 A3: 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

A4: dom p = dom q by A2, A3, FINSEQ_3:31;
thus len q = len p by A1, A3, 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: q . k = (p . k) * ((FinSeq_log 2,p) . k) by A3, A5, RVSUM_1:86;
A7: k in dom (FinSeq_log 2,p) by A1, A2, A3, A5, FINSEQ_3:31;

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

now

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 A11, A13, RVSUM_1:86;

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 A11, A13, RVSUM_1:86
.= q . k by A9, A13 ;
:: thesis: verum

end;

end;

end;

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