let p, q be ProbFinS FinSequence of REAL ; :: thesis: Entropy_of_Joint_Prob ((ColVec2Mx p) * (LineVec2Mx q)) = (Entropy p) + (Entropy q)
set M = (ColVec2Mx p) * (LineVec2Mx q);
reconsider M = (ColVec2Mx p) * (LineVec2Mx q) as Joint_Probability Matrix of REAL by Th23;
set pp = Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q));
reconsider pp = Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q)) as ProbFinS FinSequence of REAL by Th45;
(Entropy p) + (Entropy q) = - ((Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)))
.= - (SumAll (Infor_FinSeq_of M)) by Th60
.= - (Sum (Mx2FinS (Infor_FinSeq_of M))) by Th42
.= - (Sum (Infor_FinSeq_of pp)) by Th59 ;
hence Entropy_of_Joint_Prob ((ColVec2Mx p) * (LineVec2Mx q)) = (Entropy p) + (Entropy q) ; :: thesis: verum