set e = ColSum M;
set m = width M;
A6: len (ColSum M) = width M by Def2;
A7: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) >= 0 by Def6;
A8: for i being Nat st i in dom (ColSum M) holds
(ColSum M) . i >= 0

proof

let i be Nat; :: thesis: ( i in dom (ColSum M) implies (ColSum M) . i >= 0 )
assume i in dom (ColSum M) ; :: thesis: (ColSum M) . i >= 0
then A9: i in Seg (width M) by A6, FINSEQ_1:def 3;
then for j being Nat st j in dom (Col (M,i)) holds
(Col (M,i)) . j >= 0 by A7, Lm3;
then Sum (Col (M,i)) >= 0 by RVSUM_1:84;
hence (ColSum M) . i >= 0 by A9, Def2; :: thesis: verum

end;

A10: len (ColSum M) = width M by Def2;
Sum (ColSum M) = SumAll M by Th29
.= 1 by Def7 ;
hence ( not Column_Marginal M is empty & Column_Marginal M is ProbFinS ) by A10, A8, Th54; :: thesis: verum