let e be real-valued FinSequence; :: thesis: ( ( for i being Nat st i in dom e holds
0 <= e . i ) implies for k being Nat st k in dom e holds
e . k <= Sum e )
assume A1: for i being Nat st i in dom e holds
0 <= e . i ; :: thesis: for k being Nat st k in dom e holds
e . k <= Sum e

per cases ( len e = 0 or len e <> 0 ) ;

suppose len e = 0 ; :: thesis: for k being Nat st k in dom e holds
e . k <= Sum e

then e = {} ;
hence for k being Nat st k in dom e holds
e . k <= Sum e ; :: thesis: verum

end;

suppose A2: len e <> 0 ; :: thesis: for k being Nat st k in dom e holds
e . k <= Sum e

then len e >= 1 by NAT_1:14;
then A3: len e in dom e by FINSEQ_3:25;
let n be Nat; :: thesis: ( n in dom e implies e . n <= Sum e )
assume A4: n in dom e ; :: thesis: e . n <= Sum e
reconsider n = n as Nat ;
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 A2, NAT_1:14, PROB_3:63;
A8: e . n <= f . n by A1, A2, A5, A6, A4, Th4, NAT_1:14;
n <= len e by A4, FINSEQ_3:25;
then f . n <= f . (len e) by A1, A6, A4, A3, Th3;
hence e . n <= Sum e by A7, A8, XXREAL_0:2; :: thesis: verum

end;

end;