let p be ProbFinS FinSequence of REAL ; :: thesis: for M being non empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds
(Vec2DiagMx p) * M is Joint_Probability
let M be non empty-yielding Conditional_Probability Matrix of REAL ; :: thesis: ( len p = len M implies (Vec2DiagMx p) * M is Joint_Probability )
assume A1: len p = len M ; :: thesis: (Vec2DiagMx p) * M is Joint_Probability
set M1 = (Vec2DiagMx p) * M;
A2: ( len ((Vec2DiagMx p) * M) = len p & width ((Vec2DiagMx p) * M) = width M & ( for i, j being Element of NAT st [i,j] in Indices ((Vec2DiagMx p) * M) holds
((Vec2DiagMx p) * M) * i,j = (p . i) * (M * i,j) ) ) by A1, Th26;
A3: (Vec2DiagMx p) * M is m-nonnegative

proof

now

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices ((Vec2DiagMx p) * M) implies ((Vec2DiagMx p) * M) * i,j >= 0 )
assume A4: [i,j] in Indices ((Vec2DiagMx p) * M) ; :: thesis: ((Vec2DiagMx p) * M) * i,j >= 0
( i in Seg (len p) & i in Seg (len M) & j in Seg (width M) ) by A1, A2, A4, MATRPROB:12;
then ( i in dom p & [i,j] in Indices M ) by FINSEQ_1:def 3, MATRPROB:12;
then A5: ( p . i >= 0 & M * i,j >= 0 ) by MATRPROB:def 5, MATRPROB:def 6;
((Vec2DiagMx p) * M) * i,j = (p . i) * (M * i,j) by A1, A4, Th26;
hence ((Vec2DiagMx p) * M) * i,j >= 0 by A5; :: thesis: verum

end;

hence (Vec2DiagMx p) * M is m-nonnegative by MATRPROB:def 6; :: thesis: verum

end;

(Vec2DiagMx p) * M is with_sum=1

proof

A6: LineSum ((Vec2DiagMx p) * M) = p

proof

set M2 = LineSum ((Vec2DiagMx p) * M);
A7: ( len (LineSum ((Vec2DiagMx p) * M)) = len ((Vec2DiagMx p) * M) & ( for k being Element of NAT st k in Seg (len ((Vec2DiagMx p) * M)) holds
(LineSum ((Vec2DiagMx p) * M)) . k = Sum (Line ((Vec2DiagMx p) * M),k) ) ) by MATRPROB:20;
then A8: ( dom (LineSum ((Vec2DiagMx p) * M)) = dom ((Vec2DiagMx p) * M) & dom (LineSum ((Vec2DiagMx p) * M)) = dom M & dom (LineSum ((Vec2DiagMx p) * M)) = dom p ) by A1, A2, FINSEQ_3:31;

now

let k be Nat; :: thesis: ( k in dom (LineSum ((Vec2DiagMx p) * M)) implies (LineSum ((Vec2DiagMx p) * M)) . k = p . k )
assume A9: k in dom (LineSum ((Vec2DiagMx p) * M)) ; :: thesis: (LineSum ((Vec2DiagMx p) * M)) . k = p . k
k in Seg (len ((Vec2DiagMx p) * M)) by A7, A9, 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, A8, A9, Th27
.= (p . k) * (Sum (Line M,k)) by RVSUM_1:117
.= (p . k) * (Sum (M . k)) by A8, A9, MATRIX_2:18
.= (p . k) * 1 by A8, A9, MATRPROB:def 9
.= p . k ;
:: thesis: verum

end;

hence LineSum ((Vec2DiagMx p) * M) = p by A8, FINSEQ_1:17; :: thesis: verum

end;

SumAll ((Vec2DiagMx p) * M) = Sum (LineSum ((Vec2DiagMx p) * M)) by MATRPROB:def 3
.= 1 by A6, MATRPROB:def 5 ;
hence (Vec2DiagMx p) * M is with_sum=1 by MATRPROB:def 7; :: thesis: verum

end;

hence (Vec2DiagMx p) * M is Joint_Probability by A3; :: thesis: verum