let p be FinSequence of REAL ; :: thesis: ( p is ProbFinS implies ( not p is empty & p is nonnegative ) )
assume A1: p is ProbFinS ; :: thesis: ( not p is empty & p is nonnegative )
hence not p is empty by MATRPROB:def 5, RVSUM_1:102; :: thesis: p is nonnegative
for i being Element of NAT st i in dom p holds
p . i >= 0 by A1, MATRPROB:def 5;
hence p is nonnegative by Def1; :: thesis: verum