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 by Th22;
A2: LineSum ((ColVec2Mx p) * (LineVec2Mx q)) = p

proof

set M1 = LineSum ((ColVec2Mx p) * (LineVec2Mx q));
A3: len (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) = len ((ColVec2Mx p) * (LineVec2Mx q)) by MATRPROB:20;
then A4: dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) = dom ((ColVec2Mx p) * (LineVec2Mx q)) by FINSEQ_3:31;

A5: now

let k be Nat; :: thesis: ( k in dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) implies (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) . k = p . k )
assume A6: 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 A3, A6, 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 A4, A6, Th22
.= (p . k) * (Sum q) by RVSUM_1:117
.= (p . k) * 1 by MATRPROB:def 5
.= p . k ;
:: thesis: verum

end;

dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) = dom p by A1, A3, FINSEQ_3:31;
hence LineSum ((ColVec2Mx p) * (LineVec2Mx q)) = p by A5, FINSEQ_1:17; :: thesis: verum

end;

A7: width ((ColVec2Mx p) * (LineVec2Mx q)) = len q by Th22;

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 A8: [i,j] in Indices ((ColVec2Mx p) * (LineVec2Mx q)) ; :: thesis: ((ColVec2Mx p) * (LineVec2Mx q)) * i,j >= 0
i in Seg (len p) by A1, A8, MATRPROB:12;
then i in dom p by FINSEQ_1:def 3;
then A9: p . i >= 0 by MATRPROB:def 5;
j in Seg (len q) by A7, A8, MATRPROB:12;
then j in dom q by FINSEQ_1:def 3;
then A10: q . j >= 0 by MATRPROB:def 5;
((ColVec2Mx p) * (LineVec2Mx q)) * i,j = (p . i) * (q . j) by A8, Th21;
hence ((ColVec2Mx p) * (LineVec2Mx q)) * i,j >= 0 by A9, A10; :: thesis: verum

end;

then A11: (ColVec2Mx p) * (LineVec2Mx q) is m-nonnegative by MATRPROB:def 6;
SumAll ((ColVec2Mx p) * (LineVec2Mx q)) = Sum (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) by MATRPROB:def 3
.= 1 by A2, MATRPROB:def 5 ;
then (ColVec2Mx p) * (LineVec2Mx q) is with_sum=1 by MATRPROB:def 7;
hence (ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability by A11; :: thesis: verum