theorem :: ENTROPY1:46

for p being ProbFinS FinSequence of REAL
for M being empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds
Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS by Th28, Th44;