let p, q be ProbFinS FinSequence of REAL ; :: thesis: (ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability
set M = (ColVec2Mx p) * (LineVec2Mx q);
A1: ( len ((ColVec2Mx p) * (LineVec2Mx q)) = len p & width ((ColVec2Mx p) * (LineVec2Mx q)) = len q & ( for i being Element of NAT st i in dom ((ColVec2Mx p) * (LineVec2Mx q)) holds
Line ((ColVec2Mx p) * (LineVec2Mx q)),i = (p . i) * q ) ) by Th22;
A2: (ColVec2Mx p) * (LineVec2Mx q) is m-nonnegative

proof

now

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices ((ColVec2Mx p) * (LineVec2Mx q)) implies ((ColVec2Mx p) * (LineVec2Mx q)) * i,j >= 0 )
assume A3: [i,j] in Indices ((ColVec2Mx p) * (LineVec2Mx q)) ; :: thesis: ((ColVec2Mx p) * (LineVec2Mx q)) * i,j >= 0
( i in Seg (len p) & j in Seg (len q) ) by A1, A3, MATRPROB:12;
then ( i in dom p & j in dom q ) by FINSEQ_1:def 3;
then A4: ( p . i >= 0 & q . j >= 0 ) by MATRPROB:def 5;
((ColVec2Mx p) * (LineVec2Mx q)) * i,j = (p . i) * (q . j) by A3, Th21;
hence ((ColVec2Mx p) * (LineVec2Mx q)) * i,j >= 0 by A4; :: thesis: verum

end;

hence (ColVec2Mx p) * (LineVec2Mx q) is m-nonnegative by MATRPROB:def 6; :: thesis: verum

end;

(ColVec2Mx p) * (LineVec2Mx q) is with_sum=1

proof

A5: LineSum ((ColVec2Mx p) * (LineVec2Mx q)) = p

proof

set M1 = LineSum ((ColVec2Mx p) * (LineVec2Mx q));
A6: ( len (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) = len ((ColVec2Mx p) * (LineVec2Mx q)) & ( for k being Element of NAT st k in Seg (len ((ColVec2Mx p) * (LineVec2Mx q))) holds
(LineSum ((ColVec2Mx p) * (LineVec2Mx q))) . k = Sum (Line ((ColVec2Mx p) * (LineVec2Mx q)),k) ) ) by MATRPROB:20;
then A7: ( dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) = dom p & dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) = dom ((ColVec2Mx p) * (LineVec2Mx q)) ) by A1, FINSEQ_3:31;

now

let k be Nat; :: thesis: ( k in dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) implies (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) . k = p . k )
assume A8: k in dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) ; :: thesis: (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) . k = p . k
k in Seg (len ((ColVec2Mx p) * (LineVec2Mx q))) by A6, A8, FINSEQ_1:def 3;
hence (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) . k = Sum (Line ((ColVec2Mx p) * (LineVec2Mx q)),k) by MATRPROB:20
.= Sum ((p . k) * q) by A7, A8, Th22
.= (p . k) * (Sum q) by RVSUM_1:117
.= (p . k) * 1 by MATRPROB:def 5
.= p . k ;
:: thesis: verum

end;

hence LineSum ((ColVec2Mx p) * (LineVec2Mx q)) = p by A7, FINSEQ_1:17; :: thesis: verum

end;

SumAll ((ColVec2Mx p) * (LineVec2Mx q)) = Sum (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) by MATRPROB:def 3
.= 1 by A5, MATRPROB:def 5 ;
hence (ColVec2Mx p) * (LineVec2Mx q) is with_sum=1 by MATRPROB:def 7; :: thesis: verum

end;

hence (ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability by A2; :: thesis: verum