let n be non zero Nat; :: thesis: 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 )
reconsider n = n as non zero Nat ;
consider e being FinSequence of REAL such that
A1: len e = n and
A2: for i being Nat st i in Seg n holds
( ( i in Seg 1 implies e . i = jj ) & ( not i in Seg 1 implies e . i = zz ) ) by Th2;
A3: n >= 1 by NAT_1:14;
A4: Sum e = 1

proof

consider f being Real_Sequence such that
A5: f . 1 = e . 1 and
A6: for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) and
A7: Sum e = f . (len e) by A1, NAT_1:14, PROB_3:63;
for n being Nat st n <> 0 & n <= len e holds
f . n = 1

proof

defpred S₁[ Nat] means ( $1 <> 0 & $1 <= len e implies f . $1 = 1 );

A8: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( k + 1 <> 0 & k + 1 <= len e implies f . (k + 1) = 1 )

assume that
k + 1 <> 0 and
A10: k + 1 <= len e ; :: thesis: f . (k + 1) = 1

per cases ( ( k = 0 & k < len e ) or ( k > 0 & k < len e ) ) by A10, NAT_1:13;

suppose A11: ( k = 0 & k < len e ) ; :: thesis: f . (k + 1) = 1

( 1 in Seg 1 & 1 in Seg n ) by A3;
hence f . (k + 1) = 1 by A2, A5, A11; :: thesis: verum

end;

suppose A12: ( k > 0 & k < len e ) ; :: thesis: f . (k + 1) = 1

then k >= 1 by NAT_1:14;
then k + 1 > 1 by NAT_1:13;
then A13: ( k + 1 in Seg n & not k + 1 in Seg 1 ) by A1, A10, FINSEQ_1:1;
thus f . (k + 1) = 1 + (e . (k + 1)) by A6, A9, A12
.= 1 + 0 by A2, A13
.= 1 ; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A14: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A8);
hence for n being Nat st n <> 0 & n <= len e holds
f . n = 1 ; :: thesis: verum

end;

hence Sum e = 1 by A1, A7; :: thesis: verum

end;

take e ; :: thesis: ( len e = n & ( for i being Nat st i in dom e holds
e . i >= 0 ) & Sum e = 1 )
for i being Nat st i in dom e holds
e . i >= 0

proof

let i be Nat; :: thesis: ( i in dom e implies e . i >= 0 )
assume i in dom e ; :: thesis: e . i >= 0
then i in Seg n by A1, FINSEQ_1:def 3;
hence e . i >= 0 by A2; :: thesis: verum

end;

hence ( len e = n & ( for i being Nat st i in dom e holds
e . i >= 0 ) & Sum e = 1 ) by A1, A4; :: thesis: verum