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,(1 / (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,(1 / (p . k)))) ) ) )
set p0 = Infor_FinSeq_of p;

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

assume A1: 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,(1 / (p . k)))) ) )
then A2: dom q = dom (Infor_FinSeq_of p) by VALUED_1:8;
A3: Seg (len q) = dom q by FINSEQ_1:def 3
.= Seg (len (Infor_FinSeq_of p)) by A2, FINSEQ_1:def 3
.= Seg (len p) by Th47 ;
for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(1 / (p . k))))

proof

let k be Nat; :: thesis: ( k in dom q implies q . k = (p . k) * (log (2,(1 / (p . k)))) )
assume A4: k in dom q ; :: thesis: q . k = (p . k) * (log (2,(1 / (p . k))))
k in Seg (len q) by A4, FINSEQ_1:def 3;
then A5: k in dom p by A3, FINSEQ_1:def 3;
A6: q . k = - ((Infor_FinSeq_of p) . k) by A1, RVSUM_1:17;
then A7: q . k = - ((p . k) * (log (2,(p . k)))) by A2, A4, Th47
.= (p . k) * (- (log (2,(p . k)))) ;

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

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

then (Infor_FinSeq_of p) . k = 0 by A5, Th48;
hence q . k = (p . k) * (log (2,(1 / (p . k)))) by A6, A8; :: thesis: verum

end;

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

hence q . k = (p . k) * (log (2,(1 / (p . k)))) by A7, Th5; :: thesis: verum

end;

end;

end;

hence ( len q = len p & ( for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(1 / (p . k)))) ) ) by A3, FINSEQ_1:6; :: thesis: verum

end;

assume that
A9: len q = len p and
A10: for k being Nat st k in dom q holds
q . k = (p . k) * (log (2,(1 / (p . k)))) ; :: thesis: q = - (Infor_FinSeq_of p)
A11: dom q = Seg (len q) by FINSEQ_1:def 3
.= Seg (len (Infor_FinSeq_of p)) by A9, Th47
.= dom (Infor_FinSeq_of p) by FINSEQ_1:def 3 ;
A12: for k being Nat st k in dom q holds
(- (Infor_FinSeq_of p)) . k = q . k

proof

let k be Nat; :: thesis: ( k in dom q implies (- (Infor_FinSeq_of p)) . k = q . k )
assume A13: k in dom q ; :: thesis: (- (Infor_FinSeq_of p)) . k = q . k
then k in Seg (len p) by A9, FINSEQ_1:def 3;
then A14: k in dom p by FINSEQ_1:def 3;

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

suppose A15: p . k = 0 ; :: thesis: (- (Infor_FinSeq_of p)) . k = q . k

thus (- (Infor_FinSeq_of p)) . k = - ((Infor_FinSeq_of p) . k) by RVSUM_1:17
.= - 0 by A14, A15, Th48
.= (p . k) * (log (2,(1 / (p . k)))) by A15
.= q . k by A10, A13 ; :: thesis: verum

end;

suppose A16: p . k > 0 ; :: thesis: (- (Infor_FinSeq_of p)) . k = q . k

thus (- (Infor_FinSeq_of p)) . k = - ((Infor_FinSeq_of p) . k) by RVSUM_1:17
.= - ((p . k) * (log (2,(p . k)))) by A11, A13, Th47
.= (p . k) * (- (log (2,(p . k))))
.= (p . k) * (log (2,(1 / (p . k)))) by A16, Th5
.= q . k by A10, A13 ; :: thesis: verum

end;

end;

end;

dom q = dom (- (Infor_FinSeq_of p)) by A11, VALUED_1:8;
hence q = - (Infor_FinSeq_of p) by A12, FINSEQ_1:13; :: thesis: verum