theorem :: MATRPROB:53

for p being non empty real-valued ProbFinS FinSequence
for k being Nat st k in dom p holds
p . k <= 1