let seq be ExtREAL_sequence; :: thesis: ( seq is summable implies - seq is summable )
assume seq is summable ; :: thesis: - seq is summable
then A1: Partial_Sums seq is convergent by MESFUNC9:def 2;
Partial_Sums (- seq) = - (Partial_Sums seq) by Th44;
hence - seq is summable by A1, DBLSEQ_3:17, MESFUNC9:def 2; :: thesis: verum