let s1, s2 be Real_Sequence; :: thesis: ( s1 is summable & s2 is summable implies ( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) ) )

assume ( s1 is summable & s2 is summable ) ; :: thesis: ( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) )

then A1: ( Partial_Sums s1 is convergent & Partial_Sums s2 is convergent ) ;

then (Partial_Sums s1) + (Partial_Sums s2) is convergent ;

then Partial_Sums (s1 + s2) is convergent by Th5;

hence s1 + s2 is summable ; :: thesis: Sum (s1 + s2) = (Sum s1) + (Sum s2)

thus Sum (s1 + s2) = lim ((Partial_Sums s1) + (Partial_Sums s2)) by Th5

.= (Sum s1) + (Sum s2) by A1, SEQ_2:6 ; :: thesis: verum

assume ( s1 is summable & s2 is summable ) ; :: thesis: ( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) )

then A1: ( Partial_Sums s1 is convergent & Partial_Sums s2 is convergent ) ;

then (Partial_Sums s1) + (Partial_Sums s2) is convergent ;

then Partial_Sums (s1 + s2) is convergent by Th5;

hence s1 + s2 is summable ; :: thesis: Sum (s1 + s2) = (Sum s1) + (Sum s2)

thus Sum (s1 + s2) = lim ((Partial_Sums s1) + (Partial_Sums s2)) by Th5

.= (Sum s1) + (Sum s2) by A1, SEQ_2:6 ; :: thesis: verum