let p be non empty ProbFinS FinSequence of REAL ; :: thesis: for M being non empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds
Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS
let M be non empty-yielding Conditional_Probability Matrix of REAL ; :: thesis: ( len p = len M implies Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS )
assume len p = len M ; :: thesis: Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS
then (Vec2DiagMx p) * M is Joint_Probability Matrix of REAL by Th28;
hence Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS by Th44; :: thesis: verum