let p be ProbFinS FinSequence of REAL ; :: thesis: for M being 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 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;
A3: len M1 = len p by A1, A2, Th26;
then A4: dom M1 = dom p by FINSEQ_3:29;
set M2 = Infor_FinSeq_of M1;
set L = LineSum (Infor_FinSeq_of M1);
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) by FINSEQ_3:29;
A7: len (Infor_FinSeq_of M1) = len M1 by Def8;
then A8: dom (Infor_FinSeq_of M1) = dom M1 by FINSEQ_3:29;
A9: dom p = dom M by A1, FINSEQ_3:29;
A10: for k being 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 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 A11: 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, A11, Th19;
A12: p . k >= 0 by A6, A8, A4, A11, Def1;
reconsider q = Line (M,k) as non empty ProbFinS FinSequence of REAL by A6, A8, A4, A9, A11, MATRPROB:60;
A13: pp = (p . k) * q by A1, A2, A6, A8, A11, Th27;
dom (((p . k) * (log (2,(p . k)))) * q) = dom q by VALUED_1:def 5;
then A14: len (((p . k) * (log (2,(p . k)))) * q) = len q by FINSEQ_3:29;
len (FinSeq_log (2,q)) = len q by Def6;
then A15: len (mlt (q,(FinSeq_log (2,q)))) = len q by MATRPROB:30;
dom ((p . k) * (mlt (q,(FinSeq_log (2,q))))) = dom (mlt (q,(FinSeq_log (2,q)))) by VALUED_1:def 5;
then A16: len ((p . k) * (mlt (q,(FinSeq_log (2,q))))) = len (mlt (q,(FinSeq_log (2,q)))) by FINSEQ_3:29;
(LineSum (Infor_FinSeq_of M1)) . k = Sum ((Infor_FinSeq_of M1) . k) by A11, MATRPROB:def 1
.= Sum (Line ((Infor_FinSeq_of M1),k)) by A6, A11, MATRIX_0:60
.= Sum (Infor_FinSeq_of pp) by A6, A8, A11, Th53
.= Sum ((((p . k) * (log (2,(p . k)))) * q) + ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by A13, A12, Th51
.= (Sum (((p . k) * (log (2,(p . k)))) * q)) + (Sum ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by A15, A14, A16, INTEGRA5:2
.= (((p . k) * (log (2,(p . k)))) * (Sum q)) + (Sum ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by RVSUM_1:87
.= (((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:87 ;
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);
set p2 = mlt (p,(LineSum (Infor_FinSeq_of M)));
set p1 = Infor_FinSeq_of p;
A17: len (Infor_FinSeq_of p) = len p by Th47;
then A18: dom (Infor_FinSeq_of p) = dom M by A1, FINSEQ_3:29;
A19: len (Infor_FinSeq_of M) = len M by Def8;
then A20: len (LineSum (Infor_FinSeq_of M)) = len p by A1, MATRPROB:def 1;
then A21: len (mlt (p,(LineSum (Infor_FinSeq_of M)))) = len p by MATRPROB:30;
A22: dom (Infor_FinSeq_of p) = dom (Infor_FinSeq_of M) by A1, A19, A17, FINSEQ_3:29;
A23: dom (LineSum (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of p) by A20, A17, FINSEQ_3:29;
A24: dom (Infor_FinSeq_of p) = dom (LineSum (Infor_FinSeq_of M1)) by A3, A7, A5, A17, FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom (Infor_FinSeq_of p) holds
(LineSum (Infor_FinSeq_of M1)) . k = ((Infor_FinSeq_of p) . k) + ((mlt (p,(LineSum (Infor_FinSeq_of M)))) . k)

let k be 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 A25: 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)
A26: (mlt (p,(LineSum (Infor_FinSeq_of M)))) . k = (p . k) * ((LineSum (Infor_FinSeq_of M)) . k) by RVSUM_1:59
.= (p . k) * (Sum ((Infor_FinSeq_of M) . k)) by A23, A25, MATRPROB:def 1
.= (p . k) * (Sum (Line ((Infor_FinSeq_of M),k))) by A22, A25, MATRIX_0:60
.= (p . k) * (Sum (Infor_FinSeq_of (Line (M,k)))) by A18, A25, Th53 ;
thus (LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k))))) by A10, A24, A25
.= ((Infor_FinSeq_of p) . k) + ((mlt (p,(LineSum (Infor_FinSeq_of M)))) . k) by A25, A26, 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, A7, A5, A17, A21, 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