set n = 1;
set m = 1;
consider M being Matrix of 1,1,REAL such that
A1: M is m-nonnegative and
A2: SumAll M = 1 by Th55;
take M ; :: thesis: ( M is empty-yielding & M is Joint_Probability )
A3: M is with_sum=1 by A2;
A4: len M = 1 by MATRIX_0:def 2;
then width M = 1 by MATRIX_0:20;
hence ( M is empty-yielding & M is Joint_Probability ) by A1, A4, A3, MATRIX_0:def 10; :: thesis: verum