theorem :: MATRPROB:59

for M being empty-yielding Conditional_Probability Matrix of REAL
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) <= 1