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: ( not M is empty-yielding & M is Joint_Probability )
A3: M is with_sum=1 by A2, Def7;
A4: len M = 1 by MATRIX_1:def 3;
then width M = 1 by MATRIX_1:20;
hence ( not M is empty-yielding & M is Joint_Probability ) by A1, A4, A3, GOBOARD1:def 5; :: thesis: verum