let seq be Real_Sequence; :: thesis: ( seq is empty-yielding implies seq is absolutely_summable )
assume seq is empty-yielding ; :: thesis: seq is absolutely_summable
then for x being Nat holds seq . x = 0 ;
hence seq is absolutely_summable by COMSEQ_3:3; :: thesis: verum