:: deftheorem Def5 defines ProbFinS MATRPROB:def 5 :
for p being real-valued FinSequence holds
( p is ProbFinS iff ( ( for i being Nat st i in dom p holds
p . i >= 0 ) & Sum p = 1 ) );