for n being non zero Nat ex P being FinSequence of REAL st
( len P = n & ( for i being Nat st i in dom P holds
P . i >= 0 ) & Sum P = 1 )