let X be RealUnitarySpace; :: 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 by A1, Def2;
A4: Partial_Sums seq2 is convergent by A2, Def2;
then (Partial_Sums seq1) - (Partial_Sums seq2) is convergent by A3, BHSP_2:4;
then Partial_Sums (seq1 - seq2) is convergent by Th2;
hence seq1 - seq2 is summable by Def2; :: thesis: Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2)
thus Sum (seq1 - seq2) = lim ((Partial_Sums seq1) - (Partial_Sums seq2)) by Th2
.= (Sum seq1) - (Sum seq2) by A3, A4, BHSP_2:14 ; :: thesis: verum