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