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

hereby :: thesis: ( len q = len p & ( for k being Element of 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 Element of NAT st k in dom q holds
q . k = (p . k) * (log 2,(1 / (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,(1 / (p . k))) ) ) :: thesis: verum

proof

A2: dom q = dom (Infor_FinSeq_of p) by A1, 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 ;
hence len q = len p by FINSEQ_1:8; :: thesis: for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log 2,(1 / (p . k)))
thus for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log 2,(1 / (p . k))) :: thesis: verum

proof

let k be Element of 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:35;
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;

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,(1 / (p . k))) ) ) ; :: thesis: q = - (Infor_FinSeq_of p)
A10: 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 ;
then A11: dom q = dom (- (Infor_FinSeq_of p)) by VALUED_1:8;
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 A12: 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 A13: k in dom p by FINSEQ_1:def 3;

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

suppose A14: 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:35
.= - 0 by A13, A14, Th48
.= (p . k) * (log 2,(1 / (p . k))) by A14
.= q . k by A9, A12 ; :: thesis: verum

end;

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:35
.= - ((p . k) * (log 2,(p . k))) by A10, A12, Th47
.= (p . k) * (- (log 2,(p . k)))
.= (p . k) * (log 2,(1 / (p . k))) by A15, Th5
.= q . k by A9, A12 ; :: thesis: verum

end;

end;

end;

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