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

(Ser F) . r <= (Ser F) . n

y <= (Ser F) . n

(Ser F) . n9 in rng (Ser F) by FUNCT_2:4;

hence SUM F = (Ser F) . n by A14, XXREAL_2:55; :: thesis: verum

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

A9:
for r being Element of NAT st r <= n holds
defpred S_{1}[ 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_{1}[s] holds

S_{1}[s + 1]
_{1}[ 0 ]
;

for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A8, A5);

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

end;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

proof

A8:
S
let s be Nat; :: thesis: ( S_{1}[s] implies S_{1}[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_{1}[s + 1]

hence S_{1}[s + 1]
by A6, A7, XXREAL_3:4; :: thesis: verum

end;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

hence S

for m being Nat holds S

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

(Ser F) . r <= (Ser F) . n

proof

for y being ExtReal st y in rng (Ser F) holds
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;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

y <= (Ser F) . n

proof

then A14:
(Ser F) . n is UpperBound of rng (Ser F)
by XXREAL_2:def 1;
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;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

(Ser F) . n9 in rng (Ser F) by FUNCT_2:4;

hence SUM F = (Ser F) . n by A14, XXREAL_2:55; :: thesis: verum