set n = len M;
set m = width M;
A8: ( len M > 0 & width M > 0 ) by Th54;
A9: for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j >= 0 by Def6;
set e = ColSum M;
A10: ( len (ColSum M) = width M & ( for k being Element of NAT st k in Seg (width M) holds
(ColSum M) . k = Sum (Col M,k) ) ) by Def2;
A11: len (ColSum M) = width M by Def2;
A12: for i being Element of NAT st i in dom (ColSum M) holds
(ColSum M) . i >= 0

proof

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

end;

Sum (ColSum M) = SumAll M by Th29
.= 1 by Def7 ;
hence ( not Column_Marginal M is empty & Column_Marginal M is ProbFinS ) by A8, A11, A12, Def5; :: thesis: verum