set n = 1;
set m = 1;
consider M being Matrix of 1,1, REAL such that
A1: ( M is m-nonnegative & M is with_line_sum=1 ) by Th58;
take M ; :: thesis: ( not M is empty-yielding & M is Conditional_Probability )
A2: len M = 1 by MATRIX_1:def 3;
then width M = 1 by MATRIX_1:20;
hence ( not M is empty-yielding & M is Conditional_Probability ) by A1, A2, GOBOARD1:def 5; :: thesis: verum