let p, q be ProbFinS FinSequence of REAL ; :: thesis: for M being Matrix of REAL st M = (ColVec2Mx p) * (LineVec2Mx q) holds
SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q))
set p1 = Infor_FinSeq_of p;
set p2 = (Sum (Infor_FinSeq_of q)) * p;
A1: len (Infor_FinSeq_of p) = len p by Th47;
dom ((Sum (Infor_FinSeq_of q)) * p) = dom p by VALUED_1:def 5;
then A2: len (Infor_FinSeq_of p) = len ((Sum (Infor_FinSeq_of q)) * p) by A1, FINSEQ_3:29;
len (FinSeq_log (2,q)) = len q by Def6;
then A3: len (mlt (q,(FinSeq_log (2,q)))) = len q by MATRPROB:30;
let M be Matrix of REAL; :: thesis: ( M = (ColVec2Mx p) * (LineVec2Mx q) implies SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)) )
assume A4: M = (ColVec2Mx p) * (LineVec2Mx q) ; :: thesis: SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q))
reconsider M = M as Joint_Probability Matrix of REAL by A4, Th23;
set M1 = Infor_FinSeq_of M;
set L = LineSum (Infor_FinSeq_of M);
A5: len (LineSum (Infor_FinSeq_of M)) = len (Infor_FinSeq_of M) by MATRPROB:def 1;
then A6: dom (LineSum (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of M) by FINSEQ_3:29;
A7: len (Infor_FinSeq_of M) = len M by Def8;
then A8: dom (Infor_FinSeq_of M) = dom M by FINSEQ_3:29;
A9: len M = len p by A4, Th22;
then A10: dom M = dom p by FINSEQ_3:29;

A11: now :: thesis: for k being Nat st k in dom (LineSum (Infor_FinSeq_of M)) holds
(LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q)))

let k be Nat; :: thesis: ( k in dom (LineSum (Infor_FinSeq_of M)) implies (LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q))) )
assume A12: k in dom (LineSum (Infor_FinSeq_of M)) ; :: thesis: (LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q)))
reconsider pp = Line (M,k) as nonnegative FinSequence of REAL by A6, A8, A12, Th19;
A13: pp = (p . k) * q by A4, A6, A8, A12, Th22;
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;
dom ((p . k) * (mlt (q,(FinSeq_log (2,q))))) = dom (mlt (q,(FinSeq_log (2,q)))) by VALUED_1:def 5;
then A15: len (((p . k) * (log (2,(p . k)))) * q) = len ((p . k) * (mlt (q,(FinSeq_log (2,q))))) by A3, A14, FINSEQ_3:29;
A16: p . k >= 0 by A6, A8, A10, A12, Def1;
thus (LineSum (Infor_FinSeq_of M)) . k = Sum ((Infor_FinSeq_of M) . k) by A12, MATRPROB:def 1
.= Sum (Line ((Infor_FinSeq_of M),k)) by A6, A12, MATRIX_0:60
.= Sum (Infor_FinSeq_of pp) by A6, A8, A12, Th53
.= Sum ((((p . k) * (log (2,(p . k)))) * q) + ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by A13, A16, Th51
.= (Sum (((p . k) * (log (2,(p . k)))) * q)) + (Sum ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by A15, 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 ; :: thesis: verum

end;

A17: dom (Infor_FinSeq_of p) = dom (LineSum (Infor_FinSeq_of M)) by A9, A7, A5, A1, FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom (Infor_FinSeq_of p) holds
(LineSum (Infor_FinSeq_of M)) . k = ((Infor_FinSeq_of p) . k) + (((Sum (Infor_FinSeq_of q)) * p) . k)

let k be Nat; :: thesis: ( k in dom (Infor_FinSeq_of p) implies (LineSum (Infor_FinSeq_of M)) . k = ((Infor_FinSeq_of p) . k) + (((Sum (Infor_FinSeq_of q)) * p) . k) )
assume A18: k in dom (Infor_FinSeq_of p) ; :: thesis: (LineSum (Infor_FinSeq_of M)) . k = ((Infor_FinSeq_of p) . k) + (((Sum (Infor_FinSeq_of q)) * p) . k)
thus (LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q))) by A11, A17, A18
.= ((Infor_FinSeq_of p) . k) + ((p . k) * (Sum (Infor_FinSeq_of q))) by A18, Th47
.= ((Infor_FinSeq_of p) . k) + (((Sum (Infor_FinSeq_of q)) * p) . k) by RVSUM_1:44 ; :: thesis: verum

end;

then Sum (LineSum (Infor_FinSeq_of M)) = (Sum (Infor_FinSeq_of p)) + (Sum ((Sum (Infor_FinSeq_of q)) * p)) by A9, A7, A5, A1, A2, Th7
.= (Sum (Infor_FinSeq_of p)) + ((Sum (Infor_FinSeq_of q)) * (Sum p)) by RVSUM_1:87
.= (Sum (Infor_FinSeq_of p)) + ((Sum (Infor_FinSeq_of q)) * 1) by MATRPROB:def 5
.= (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)) ;
hence SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)) by MATRPROB:def 3; :: thesis: verum