theorem Th60: :: MATRPROB:60

for M being V3() Matrix of REAL holds
( M is V3() Conditional_Probability Matrix of REAL iff for i being Nat st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL )