theorem :: MATRPROB:53

for p being non empty ProbFinS FinSequence of REAL
for k being Nat st k in dom p holds
p . k <= 1