let p be ProbFinS FinSequence of REAL ; :: thesis: for M being non empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds
for M1 being Matrix of REAL st M1 = (Vec2DiagMx p) * M holds
SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt p,(LineSum (Infor_FinSeq_of M))))
let M be non empty-yielding Conditional_Probability Matrix of REAL ; :: thesis: ( len p = len M implies for M1 being Matrix of REAL st M1 = (Vec2DiagMx p) * M holds
SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt p,(LineSum (Infor_FinSeq_of M)))) )
assume A1: len p = len M ; :: thesis: for M1 being Matrix of REAL st M1 = (Vec2DiagMx p) * M holds
SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt p,(LineSum (Infor_FinSeq_of M))))
let M1 be Matrix of REAL ; :: thesis: ( M1 = (Vec2DiagMx p) * M implies SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt p,(LineSum (Infor_FinSeq_of M)))) )
assume A2: M1 = (Vec2DiagMx p) * M ; :: thesis: SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt p,(LineSum (Infor_FinSeq_of M))))
reconsider M1 = M1 as Joint_Probability Matrix of REAL by A1, A2, Th28;
set M2 = Infor_FinSeq_of M1;
set L = LineSum (Infor_FinSeq_of M1);
A3: ( len M1 = len p & width M1 = width M ) by A1, A2, Th26;
A4: ( len (Infor_FinSeq_of M1) = len M1 & width (Infor_FinSeq_of M1) = width M1 ) by Def8;
A5: len (LineSum (Infor_FinSeq_of M1)) = len (Infor_FinSeq_of M1) by MATRPROB:def 1;
then A6: ( dom (LineSum (Infor_FinSeq_of M1)) = dom (Infor_FinSeq_of M1) & dom (Infor_FinSeq_of M1) = dom M1 & dom M1 = dom p & dom p = dom M ) by A1, A3, A4, FINSEQ_3:31;
A7: for k being Element of NAT st k in dom (LineSum (Infor_FinSeq_of M1)) holds
(LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log 2,(p . k))) + ((p . k) * (Sum (Infor_FinSeq_of (Line M,k))))

proof

let k be Element of NAT ; :: thesis: ( k in dom (LineSum (Infor_FinSeq_of M1)) implies (LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log 2,(p . k))) + ((p . k) * (Sum (Infor_FinSeq_of (Line M,k)))) )
assume A8: k in dom (LineSum (Infor_FinSeq_of M1)) ; :: thesis: (LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log 2,(p . k))) + ((p . k) * (Sum (Infor_FinSeq_of (Line M,k))))
reconsider pp = Line M1,k as nonnegative FinSequence of REAL by A6, A8, Th19;
reconsider q = Line M,k as non empty ProbFinS FinSequence of REAL by A6, A8, MATRPROB:60;
len (FinSeq_log 2,q) = len q by Def6;
then A9: len (mlt q,(FinSeq_log 2,q)) = len q by MATRPROB:30;
A10: pp = (p . k) * q by A1, A2, A6, A8, Th27;
A11: p . k >= 0 by A6, A8, Def1;
dom (((p . k) * (log 2,(p . k))) * q) = dom q by VALUED_1:def 5;
then A12: len (((p . k) * (log 2,(p . k))) * q) = len q by FINSEQ_3:31;
dom ((p . k) * (mlt q,(FinSeq_log 2,q))) = dom (mlt q,(FinSeq_log 2,q)) by VALUED_1:def 5;
then A13: len ((p . k) * (mlt q,(FinSeq_log 2,q))) = len (mlt q,(FinSeq_log 2,q)) by FINSEQ_3:31;
(LineSum (Infor_FinSeq_of M1)) . k = Sum ((Infor_FinSeq_of M1) . k) by A8, MATRPROB:def 1
.= Sum (Line (Infor_FinSeq_of M1),k) by A6, A8, MATRIX_2:18
.= Sum (Infor_FinSeq_of pp) by A6, A8, Th53
.= Sum ((((p . k) * (log 2,(p . k))) * q) + ((p . k) * (mlt q,(FinSeq_log 2,q)))) by A10, A11, Th51
.= (Sum (((p . k) * (log 2,(p . k))) * q)) + (Sum ((p . k) * (mlt q,(FinSeq_log 2,q)))) by A9, A12, A13, INTEGRA5:2
.= (((p . k) * (log 2,(p . k))) * (Sum q)) + (Sum ((p . k) * (mlt q,(FinSeq_log 2,q)))) by RVSUM_1:117
.= (((p . k) * (log 2,(p . k))) * 1) + (Sum ((p . k) * (mlt q,(FinSeq_log 2,q)))) by MATRPROB:def 5
.= ((p . k) * (log 2,(p . k))) + ((p . k) * (Sum (Infor_FinSeq_of q))) by RVSUM_1:117 ;
hence (LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log 2,(p . k))) + ((p . k) * (Sum (Infor_FinSeq_of (Line M,k)))) ; :: thesis: verum

end;

set M3 = Infor_FinSeq_of M;
set L2 = LineSum (Infor_FinSeq_of M);
( len (Infor_FinSeq_of M) = len M & width (Infor_FinSeq_of M) = width M ) by Def8;
then A14: ( len (LineSum (Infor_FinSeq_of M)) = len M & len (LineSum (Infor_FinSeq_of M)) = len p & len (LineSum (Infor_FinSeq_of M)) = len (Infor_FinSeq_of M) ) by A1, MATRPROB:def 1;
set p1 = Infor_FinSeq_of p;
set p2 = mlt p,(LineSum (Infor_FinSeq_of M));
A15: len (Infor_FinSeq_of p) = len p by Th47;
A16: len (mlt p,(LineSum (Infor_FinSeq_of M))) = len p by A14, MATRPROB:30;
then A17: ( dom (Infor_FinSeq_of p) = dom (LineSum (Infor_FinSeq_of M1)) & dom (Infor_FinSeq_of p) = dom (mlt p,(LineSum (Infor_FinSeq_of M))) & dom (LineSum (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of p) & dom (Infor_FinSeq_of p) = dom (Infor_FinSeq_of M) & dom (Infor_FinSeq_of p) = dom M ) by A3, A4, A5, A14, A15, FINSEQ_3:31;

now

let k be Element of NAT ; :: thesis: ( k in dom (Infor_FinSeq_of p) implies (LineSum (Infor_FinSeq_of M1)) . k = ((Infor_FinSeq_of p) . k) + ((mlt p,(LineSum (Infor_FinSeq_of M))) . k) )
assume A18: k in dom (Infor_FinSeq_of p) ; :: thesis: (LineSum (Infor_FinSeq_of M1)) . k = ((Infor_FinSeq_of p) . k) + ((mlt p,(LineSum (Infor_FinSeq_of M))) . k)
A19: (mlt p,(LineSum (Infor_FinSeq_of M))) . k = (p . k) * ((LineSum (Infor_FinSeq_of M)) . k) by A17, A18, RVSUM_1:86
.= (p . k) * (Sum ((Infor_FinSeq_of M) . k)) by A17, A18, MATRPROB:def 1
.= (p . k) * (Sum (Line (Infor_FinSeq_of M),k)) by A17, A18, MATRIX_2:18
.= (p . k) * (Sum (Infor_FinSeq_of (Line M,k))) by A17, A18, Th53 ;
thus (LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log 2,(p . k))) + ((p . k) * (Sum (Infor_FinSeq_of (Line M,k)))) by A7, A17, A18
.= ((Infor_FinSeq_of p) . k) + ((mlt p,(LineSum (Infor_FinSeq_of M))) . k) by A18, A19, Th47 ; :: thesis: verum

end;

then Sum (LineSum (Infor_FinSeq_of M1)) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt p,(LineSum (Infor_FinSeq_of M)))) by A3, A4, A5, A15, A16, Th7;
hence SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt p,(LineSum (Infor_FinSeq_of M)))) by MATRPROB:def 3; :: thesis: verum