for p being non empty ProbFinS FinSequence of REAL
for k being Nat st k in dom p holds
(Infor_FinSeq_of p) . k <= 0