let X be RealNormSpace; :: 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 ( seq1 is summable & seq2 is summable ) ; :: thesis: ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )

then A1: ( Partial_Sums seq1 is convergent & Partial_Sums seq2 is convergent ) ;

then A2: (Partial_Sums seq1) + (Partial_Sums seq2) is convergent by NORMSP_1:19;

A3: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by Th15;

Sum (seq1 + seq2) = lim ((Partial_Sums seq1) + (Partial_Sums seq2)) by Th15

.= (lim (Partial_Sums seq1)) + (lim (Partial_Sums seq2)) by A1, NORMSP_1:25 ;

hence ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) by A2, A3; :: thesis: verum

( 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 ( seq1 is summable & seq2 is summable ) ; :: thesis: ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )

then A1: ( Partial_Sums seq1 is convergent & Partial_Sums seq2 is convergent ) ;

then A2: (Partial_Sums seq1) + (Partial_Sums seq2) is convergent by NORMSP_1:19;

A3: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by Th15;

Sum (seq1 + seq2) = lim ((Partial_Sums seq1) + (Partial_Sums seq2)) by Th15

.= (lim (Partial_Sums seq1)) + (lim (Partial_Sums seq2)) by A1, NORMSP_1:25 ;

hence ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) by A2, A3; :: thesis: verum