let M be non empty-yielding Conditional_Probability Matrix of REAL ; :: thesis: Entropy_of_Cond_Prob M = - (LineSum (Infor_FinSeq_of M))
set p = Entropy_of_Cond_Prob M;
set q = - (LineSum (Infor_FinSeq_of M));
A1: ( len (Entropy_of_Cond_Prob M) = len M & ( for k being Element of NAT st k in dom (Entropy_of_Cond_Prob M) holds
(Entropy_of_Cond_Prob M) . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) by Th62;
A2: dom (- (LineSum (Infor_FinSeq_of M))) = dom (LineSum (Infor_FinSeq_of M)) by VALUED_1:8;
then len (- (LineSum (Infor_FinSeq_of M))) = len (LineSum (Infor_FinSeq_of M)) by FINSEQ_3:31;
then len (- (LineSum (Infor_FinSeq_of M))) = len (Infor_FinSeq_of M) by MATRPROB:def 1;
then len (- (LineSum (Infor_FinSeq_of M))) = len M by Def8;
then A3: ( dom (Entropy_of_Cond_Prob M) = dom (- (LineSum (Infor_FinSeq_of M))) & dom (Entropy_of_Cond_Prob M) = dom M ) by A1, FINSEQ_3:31;

now

let k be Nat; :: thesis: ( k in dom (Entropy_of_Cond_Prob M) implies (Entropy_of_Cond_Prob M) . k = (- (LineSum (Infor_FinSeq_of M))) . k )
assume A4: k in dom (Entropy_of_Cond_Prob M) ; :: thesis: (Entropy_of_Cond_Prob M) . k = (- (LineSum (Infor_FinSeq_of M))) . k
thus (Entropy_of_Cond_Prob M) . k = - (Sum ((Infor_FinSeq_of M) . k)) by A4, Th62
.= - ((Sum (Infor_FinSeq_of M)) . k) by A2, A3, A4, MATRPROB:def 1
.= (- (LineSum (Infor_FinSeq_of M))) . k by RVSUM_1:35 ; :: thesis: verum

end;

hence Entropy_of_Cond_Prob M = - (LineSum (Infor_FinSeq_of M)) by A3, FINSEQ_1:17; :: thesis: verum