let e be FinSequence of REAL ; :: 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 by RELAT_1:60; :: thesis: verum

end;

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

then A2: len e >= 1 by NAT_1:14;
then consider f being Real_Sequence such that
A3: ( f . 1 = e . 1 & ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) & Sum e = f . (len e) ) by PROB_3:68;
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 Element of NAT by ORDINAL1:def 13;
( n <= len e & len e in dom e ) by A2, A4, FINSEQ_3:27;
then ( f . n <= f . (len e) & e . n <= f . n ) by A1, A2, A3, A4, Th3, Th4;
hence e . n <= Sum e by A3, XXREAL_0:2; :: thesis: verum

end;

end;