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