set n = 1;
consider p being FinSequence of REAL such that
A1: ( len p = 1 & ( for i being Element of NAT st i in dom p holds
p . i >= 0 ) & Sum p = 1 ) by Th52;
take p ; :: thesis: ( not p is empty & p is ProbFinS )
thus ( not p is empty & p is ProbFinS ) by A1, Def5; :: thesis: verum