consider p being FinSequence of REAL such that
A1: ( len p = 1 & ( for i being 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; :: thesis: verum