let MR be Matrix of REAL; :: thesis: ( MR is Joint_Probability iff Mx2FinS MR is ProbFinS )

hereby :: thesis: ( Mx2FinS MR is ProbFinS implies MR is Joint_Probability )

assume MR is Joint_Probability ; :: thesis: Mx2FinS MR is ProbFinS
then reconsider MRR = MR as Joint_Probability Matrix of REAL ;
A1: MRR is m-nonnegative with_sum=1 Matrix of REAL ;
then Mx2FinS MR is nonnegative by Th43;
then A2: for i being Nat st i in dom (Mx2FinS MR) holds
(Mx2FinS MR) . i >= 0 ;
Sum (Mx2FinS MR) = SumAll MR by Th42
.= 1 by A1, MATRPROB:def 7 ;
hence Mx2FinS MR is ProbFinS by A2, MATRPROB:def 5; :: thesis: verum

end;

assume Mx2FinS MR is ProbFinS ; :: thesis: MR is Joint_Probability
then reconsider pp = Mx2FinS MR as ProbFinS FinSequence of REAL ;
reconsider p = pp as non empty ProbFinS FinSequence of REAL ;
SumAll MR = Sum p by Th42
.= 1 by MATRPROB:def 5 ;
then A3: MR is with_sum=1 by MATRPROB:def 7;
p is nonnegative ;
then MR is m-nonnegative by Th43;
hence MR is Joint_Probability by A3; :: thesis: verum