let p be ProbFinS FinSequence of REAL ; :: thesis: for M being empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds
(Vec2DiagMx p) * M is Joint_Probability
let M be empty-yielding Conditional_Probability Matrix of REAL; :: thesis: ( len p = len M implies (Vec2DiagMx p) * M is Joint_Probability )
set M1 = (Vec2DiagMx p) * M;
assume A1: len p = len M ; :: thesis: (Vec2DiagMx p) * M is Joint_Probability
then A2: len ((Vec2DiagMx p) * M) = len p by Th26;
A3: LineSum ((Vec2DiagMx p) * M) = p

proof

set M2 = LineSum ((Vec2DiagMx p) * M);
A4: len (LineSum ((Vec2DiagMx p) * M)) = len ((Vec2DiagMx p) * M) by MATRPROB:20;
then A5: dom (LineSum ((Vec2DiagMx p) * M)) = dom M by A1, A2, FINSEQ_3:29;
A6: dom (LineSum ((Vec2DiagMx p) * M)) = dom ((Vec2DiagMx p) * M) by A4, FINSEQ_3:29;

A7: now :: thesis: for k being Nat st k in dom (LineSum ((Vec2DiagMx p) * M)) holds
(LineSum ((Vec2DiagMx p) * M)) . k = p . k

let k be Nat; :: thesis: ( k in dom (LineSum ((Vec2DiagMx p) * M)) implies (LineSum ((Vec2DiagMx p) * M)) . k = p . k )
assume A8: k in dom (LineSum ((Vec2DiagMx p) * M)) ; :: thesis: (LineSum ((Vec2DiagMx p) * M)) . k = p . k
k in Seg (len ((Vec2DiagMx p) * M)) by A4, A8, FINSEQ_1:def 3;
hence (LineSum ((Vec2DiagMx p) * M)) . k = Sum (Line (((Vec2DiagMx p) * M),k)) by MATRPROB:20
.= Sum ((p . k) * (Line (M,k))) by A1, A6, A8, Th27
.= (p . k) * (Sum (Line (M,k))) by RVSUM_1:87
.= (p . k) * (Sum (M . k)) by A5, A8, MATRIX_0:60
.= (p . k) * 1 by A5, A8, MATRPROB:def 9
.= p . k ;
:: thesis: verum

end;

dom (LineSum ((Vec2DiagMx p) * M)) = dom p by A2, A4, FINSEQ_3:29;
hence LineSum ((Vec2DiagMx p) * M) = p by A7, FINSEQ_1:13; :: thesis: verum

end;

A9: width ((Vec2DiagMx p) * M) = width M by A1, Th26;

now :: thesis: for i, j being Nat st [i,j] in Indices ((Vec2DiagMx p) * M) holds
((Vec2DiagMx p) * M) * (i,j) >= 0

let i, j be Nat; :: thesis: ( [i,j] in Indices ((Vec2DiagMx p) * M) implies ((Vec2DiagMx p) * M) * (i,j) >= 0 )
assume A10: [i,j] in Indices ((Vec2DiagMx p) * M) ; :: thesis: ((Vec2DiagMx p) * M) * (i,j) >= 0
A11: j in Seg (width M) by A9, A10, MATRPROB:12;
i in Seg (len p) by A2, A10, MATRPROB:12;
then i in dom p by FINSEQ_1:def 3;
then A12: p . i >= 0 by MATRPROB:def 5;
i in Seg (len M) by A1, A2, A10, MATRPROB:12;
then [i,j] in Indices M by A11, MATRPROB:12;
then A13: M * (i,j) >= 0 by MATRPROB:def 6;
((Vec2DiagMx p) * M) * (i,j) = (p . i) * (M * (i,j)) by A1, A10, Th26;
hence ((Vec2DiagMx p) * M) * (i,j) >= 0 by A12, A13; :: thesis: verum

end;

then A14: (Vec2DiagMx p) * M is m-nonnegative by MATRPROB:def 6;
SumAll ((Vec2DiagMx p) * M) = Sum (LineSum ((Vec2DiagMx p) * M)) by MATRPROB:def 3
.= 1 by A3, MATRPROB:def 5 ;
then (Vec2DiagMx p) * M is with_sum=1 by MATRPROB:def 7;
hence (Vec2DiagMx p) * M is Joint_Probability by A14; :: thesis: verum