let e be real-valued FinSequence; ( ( 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
; for k being Nat st k in dom e holds
e . k <= Sum e
per cases
( len e = 0 or len e <> 0 )
;
suppose A2:
len e <> 0
;
for k being Nat st k in dom e holds
e . k <= Sum ethen
len e >= 1
by NAT_1:14;
then A3:
len e in dom e
by FINSEQ_3:25;
let n be
Nat;
( n in dom e implies e . n <= Sum e )assume A4:
n in dom e
;
e . n <= Sum ereconsider n =
n as
Nat ;
e is
FinSequence of
REAL
by RVSUM_1:145;
then 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;
verum end; end;