A1: for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j >= 0 by Def6;
set e = LineSum M;
set n = len M;
A2: len M > 0 by Th54;
A3: ( len (LineSum M) = len M & ( for k being Element of NAT st k in Seg (len M) holds
(LineSum M) . k = Sum (Line M,k) ) ) by Th20;
A4: len (LineSum M) = len M by Th20;
A5: for i being Element of NAT st i in dom (LineSum M) holds
(LineSum M) . i >= 0

proof

let i be Element of NAT ; :: thesis: ( i in dom (LineSum M) implies (LineSum M) . i >= 0 )
assume A6: i in dom (LineSum M) ; :: thesis: (LineSum M) . i >= 0
A7: i in Seg (len M) by A3, A6, FINSEQ_1:def 3;
then i in dom M by FINSEQ_1:def 3;
then for j being Nat st j in dom (Line M,i) holds
(Line M,i) . j >= 0 by A1, Lm2;
then Sum (Line M,i) >= 0 by RVSUM_1:114;
hence (LineSum M) . i >= 0 by A7, Th20; :: thesis: verum

end;

Sum (LineSum M) = SumAll M
.= 1 by Def7 ;
hence ( not Row_Marginal M is empty & Row_Marginal M is ProbFinS ) by A2, A4, A5, Def5; :: thesis: verum