set n = len M;
set e = LineSum M;
A1: len (LineSum M) = len M by Th20;
A2: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) >= 0 by Def6;
A3: for i being Nat st i in dom (LineSum M) holds
(LineSum M) . i >= 0

proof

let i be Nat; :: thesis: ( i in dom (LineSum M) implies (LineSum M) . i >= 0 )
assume i in dom (LineSum M) ; :: thesis: (LineSum M) . i >= 0
then A4: i in Seg (len M) by A1, 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 A2, Lm2;
then Sum (Line (M,i)) >= 0 by RVSUM_1:84;
hence (LineSum M) . i >= 0 by A4, Th20; :: thesis: verum

end;

A5: Sum (LineSum M) = SumAll M
.= 1 by Def7 ;
len (LineSum M) = len M by Th20;
hence ( not Row_Marginal M is empty & Row_Marginal M is ProbFinS ) by A3, A5, Th54; :: thesis: verum