let F be sequence of ExtREAL; :: thesis: ( F is nonnegative implies for n being Nat st ( for r being Element of NAT st n <= r holds
F . r = 0. ) holds
SUM F = (Ser F) . n )
assume A1: F is nonnegative ; :: thesis: for n being Nat st ( for r being Element of NAT st n <= r holds
F . r = 0. ) holds
SUM F = (Ser F) . n
let n be Nat; :: thesis: ( ( for r being Element of NAT st n <= r holds
F . r = 0. ) implies SUM F = (Ser F) . n )
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
assume A2: for r being Element of NAT st n <= r holds
F . r = 0. ; :: thesis: SUM F = (Ser F) . n
A3: for r being Element of NAT st n <= r holds
(Ser F) . r <= (Ser F) . n

proof

defpred S₁[ Nat] means (Ser F) . (n + $1) <= (Ser F) . n;
let r be Element of NAT ; :: thesis: ( n <= r implies (Ser F) . r <= (Ser F) . n )
assume n <= r ; :: thesis: (Ser F) . r <= (Ser F) . n
then A4: ex m being Nat st r = n + m by NAT_1:10;
A5: for s being Nat st S₁[s] holds
S₁[s + 1]

proof

let s be Nat; :: thesis: ( S₁[s] implies S₁[s + 1] )
reconsider s9 = s as Element of NAT by ORDINAL1:def 12;
reconsider y = (Ser F) . (n + s) as R_eal ;
n9 + (s9 + 1) = (n9 + s9) + 1 ;
then A6: (Ser F) . (n9 + (s9 + 1)) = y + (F . (n9 + (s9 + 1))) by Def11;
n + 0 <= n + (s + 1) by XREAL_1:7;
then A7: F . (n9 + (s9 + 1)) = 0. by A2;
assume (Ser F) . (n + s) <= (Ser F) . n ; :: thesis: S₁[s + 1]
hence S₁[s + 1] by A6, A7, XXREAL_3:4; :: thesis: verum

end;

A8: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A8, A5);
hence (Ser F) . r <= (Ser F) . n by A4; :: thesis: verum

end;

A9: for r being Element of NAT st r <= n holds
(Ser F) . r <= (Ser F) . n

proof

let r be Element of NAT ; :: thesis: ( r <= n implies (Ser F) . r <= (Ser F) . n )
assume r <= n ; :: thesis: (Ser F) . r <= (Ser F) . n
then consider m being Nat such that
A10: n = r + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
thus (Ser F) . r <= (Ser F) . n by A1, Th40, A10; :: thesis: verum

end;

for y being ExtReal st y in rng (Ser F) holds
y <= (Ser F) . n

proof

let y be ExtReal; :: thesis: ( y in rng (Ser F) implies y <= (Ser F) . n )
A11: dom (Ser F) = NAT by FUNCT_2:def 1;
assume y in rng (Ser F) ; :: thesis: y <= (Ser F) . n
then consider m being object such that
A12: m in NAT and
A13: y = (Ser F) . m by A11, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A12;
( m <= n or n <= m ) ;
hence y <= (Ser F) . n by A3, A9, A13; :: thesis: verum

end;

then A14: (Ser F) . n is UpperBound of rng (Ser F) by XXREAL_2:def 1;
(Ser F) . n9 in rng (Ser F) by FUNCT_2:4;
hence SUM F = (Ser F) . n by A14, XXREAL_2:55; :: thesis: verum