let F be sequence of ExtREAL; :: thesis: ( F is nonnegative & ex n being Element of NAT st

( ( for k being Element of NAT st n <= k holds

F . k = 0. ) & ( for k being Element of NAT st k <= n holds

F . k <> +infty ) ) implies F is summable )

assume A1: F is nonnegative ; :: thesis: ( for n being Element of NAT holds

( ex k being Element of NAT st

( n <= k & not F . k = 0. ) or ex k being Element of NAT st

( k <= n & not F . k <> +infty ) ) or F is summable )

given n being Element of NAT such that A2: for k being Element of NAT st n <= k holds

F . k = 0. and

A3: for k being Element of NAT st k <= n holds

F . k <> +infty ; :: thesis: F is summable

for s being Element of NAT holds F . s in REAL

hence F is summable by A1, A2, Th47; :: thesis: verum

( ( for k being Element of NAT st n <= k holds

F . k = 0. ) & ( for k being Element of NAT st k <= n holds

F . k <> +infty ) ) implies F is summable )

assume A1: F is nonnegative ; :: thesis: ( for n being Element of NAT holds

( ex k being Element of NAT st

( n <= k & not F . k = 0. ) or ex k being Element of NAT st

( k <= n & not F . k <> +infty ) ) or F is summable )

given n being Element of NAT such that A2: for k being Element of NAT st n <= k holds

F . k = 0. and

A3: for k being Element of NAT st k <= n holds

F . k <> +infty ; :: thesis: F is summable

for s being Element of NAT holds F . s in REAL

proof

then
(Ser F) . n in REAL
by Th48;
let s be Element of NAT ; :: thesis: F . s in REAL

A4: ( s <= n implies F . s in REAL )

end;A4: ( s <= n implies F . s in REAL )

proof

( n <= s implies F . s in REAL )
A5:
F . s <> -infty
by XXREAL_0:6, A1, Th38;

assume s <= n ; :: thesis: F . s in REAL

then A6: not F . s = +infty by A3;

( F . s in REAL or F . s in {-infty,+infty} ) by XBOOLE_0:def 3;

hence F . s in REAL by A6, A5, TARSKI:def 2; :: thesis: verum

end;assume s <= n ; :: thesis: F . s in REAL

then A6: not F . s = +infty by A3;

( F . s in REAL or F . s in {-infty,+infty} ) by XBOOLE_0:def 3;

hence F . s in REAL by A6, A5, TARSKI:def 2; :: thesis: verum

proof

hence
F . s in REAL
by A4; :: thesis: verum
assume
n <= s
; :: thesis: F . s in REAL

then F . s = 0. by A2;

hence F . s in REAL by XREAL_0:def 1; :: thesis: verum

end;then F . s = 0. by A2;

hence F . s in REAL by XREAL_0:def 1; :: thesis: verum

hence F is summable by A1, A2, Th47; :: thesis: verum