let seq1, seq2 be Complex_Sequence; :: thesis: ( seq1 is summable & seq2 is summable implies ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) )
assume A1: ( seq1 is summable & seq2 is summable ) ; :: thesis: ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
then A2: (Partial_Sums seq1) - (Partial_Sums seq2) is convergent ;
A3: (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by Th28;
Sum (seq1 - seq2) = lim ((Partial_Sums seq1) - (Partial_Sums seq2)) by Th28
.= (lim (Partial_Sums seq1)) - (lim (Partial_Sums seq2)) by A1, COMSEQ_2:26 ;
hence ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) by A2, A3; :: thesis: verum