let F be Function of NAT , 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 n' = n as Element of NAT by ORDINAL1:def 13;
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

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;
defpred S₁[ Nat] means (Ser F) . (n + $1) <= (Ser F) . n;
for m being Nat holds S₁[m]

proof

A5: S₁[ 0 ] ;
A6: for s being Nat st S₁[s] holds
S₁[s + 1]

proof

let s be Nat; :: thesis: ( S₁[s] implies S₁[s + 1] )
reconsider s' = s as Element of NAT by ORDINAL1:def 13;
assume A7: (Ser F) . (n + s) <= (Ser F) . n ; :: thesis: S₁[s + 1]
A8: n' + (s' + 1) = (n' + s') + 1 ;
reconsider y = (Ser F) . (n + s) as R_eal ;
A9: (Ser F) . (n' + (s' + 1)) = y + (F . (n' + (s' + 1))) by A8, Th63;
0 <= s + 1 by NAT_1:2;
then n + 0 <= n + (s + 1) by XREAL_1:9;
then F . (n' + (s' + 1)) = 0. by A2;
hence S₁[s + 1] by A7, A9, Th18; :: thesis: verum

end;

thus for m being Nat holds S₁[m] from NAT_1:sch 2(A5, A6); :: thesis: verum

end;

hence (Ser F) . r <= (Ser F) . n by A4; :: thesis: verum

end;

A10: 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
A11: n = r + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
n = r + m by A11;
hence (Ser F) . r <= (Ser F) . n by A1, Th60; :: thesis: verum

end;

for y being ext-real number st y in rng (Ser F) holds
y <= (Ser F) . n

proof

let y be ext-real number ; :: thesis: ( y in rng (Ser F) implies y <= (Ser F) . n )
assume A12: y in rng (Ser F) ; :: thesis: y <= (Ser F) . n
( dom (Ser F) = NAT & rng (Ser F) c= ExtREAL ) by FUNCT_2:def 1;
then consider m being set such that
A13: ( m in NAT & y = (Ser F) . m ) by A12, FUNCT_1:def 5;
reconsider m = m as Element of NAT by A13;
( m <= n or n <= m ) ;
hence y <= (Ser F) . n by A3, A10, A13; :: thesis: verum

end;

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