let p be non empty real-valued ProbFinS FinSequence; :: thesis: for k being 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 Nat st k in dom p holds
p . k <= 1 by Th5; :: thesis: verum