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

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