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: ( M is V3() & M is Conditional_Probability )
A2: len M = 1 by MATRIX_0:def 2;
then width M = 1 by MATRIX_0:20;
hence ( M is V3() & M is Conditional_Probability ) by A1, A2, MATRIX_0:def 10; :: thesis: verum