let p be non empty ProbFinS FinSequence of REAL ; :: thesis: for k being Element of NAT st k in dom p holds
p . k <= 1
( Sum p = 1 & ( for i being Nat st i in dom p holds
p . i >= 0 ) ) by Def5;
hence for k being Element of NAT st k in dom p holds
p . k <= 1 by Th5; :: thesis: verum