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: 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:29;
then len (- (LineSum (Infor_FinSeq_of M))) = len (Infor_FinSeq_of M) by MATRPROB:def 1;
then A2: len (- (LineSum (Infor_FinSeq_of M))) = len M by Def8;
len (Entropy_of_Cond_Prob M) = len M by Th62;
then A3: dom (Entropy_of_Cond_Prob M) = dom (- (LineSum (Infor_FinSeq_of M))) by A2, FINSEQ_3:29;

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 A1, A3, A4, MATRPROB:def 1
.= (- (LineSum (Infor_FinSeq_of M))) . k by RVSUM_1:17 ; :: thesis: verum

end;

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