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

proof

let s be Element of NAT ; :: thesis: F . s in REAL
A4: ( s <= n implies F . s in REAL )

proof

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;

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

proof

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;

hence F . s in REAL by A4; :: thesis: verum

end;

then (Ser F) . n in REAL by Th48;
hence F is summable by A1, A2, Th47; :: thesis: verum