let X be ComplexNormSpace; :: thesis: for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is summable & seq2 is summable implies ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) )
assume that
A1: seq1 is summable and
A2: seq2 is summable ; :: thesis: ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
A3: ( Partial_Sums seq1 is convergent & Partial_Sums seq2 is convergent ) by A1, A2, Def2;
then A4: (Partial_Sums seq1) + (Partial_Sums seq2) is convergent by CLVECT_1:115;
A5: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by Th19;
Sum (seq1 + seq2) = lim ((Partial_Sums seq1) + (Partial_Sums seq2)) by Th19
.= (lim (Partial_Sums seq1)) + (lim (Partial_Sums seq2)) by A3, CLVECT_1:121 ;
hence ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) by A4, A5, Def2; :: thesis: verum