let s be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= s . n ) implies ( Partial_Sums s is bounded_above iff s is summable ) )

assume for n being Nat holds 0 <= s . n ; :: thesis: ( Partial_Sums s is bounded_above iff s is summable )

then Partial_Sums s is V47() by Th16;

hence ( Partial_Sums s is bounded_above implies s is summable ) ; :: thesis: ( s is summable implies Partial_Sums s is bounded_above )

assume s is summable ; :: thesis: Partial_Sums s is bounded_above

then Partial_Sums s is convergent ;

then Partial_Sums s is bounded ;

hence Partial_Sums s is bounded_above ; :: thesis: verum

assume for n being Nat holds 0 <= s . n ; :: thesis: ( Partial_Sums s is bounded_above iff s is summable )

then Partial_Sums s is V47() by Th16;

hence ( Partial_Sums s is bounded_above implies s is summable ) ; :: thesis: ( s is summable implies Partial_Sums s is bounded_above )

assume s is summable ; :: thesis: Partial_Sums s is bounded_above

then Partial_Sums s is convergent ;

then Partial_Sums s is bounded ;

hence Partial_Sums s is bounded_above ; :: thesis: verum