let seq1, seq2 be Complex_Sequence; :: thesis: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)
A1: Im ((Partial_Sums seq1) + (Partial_Sums seq2)) = (Im (Partial_Sums seq1)) + (Im (Partial_Sums seq2)) by Th15
.= (Partial_Sums (Im seq1)) + (Im (Partial_Sums seq2)) by Th26
.= (Partial_Sums (Im seq1)) + (Partial_Sums (Im seq2)) by Th26
.= Partial_Sums ((Im seq1) + (Im seq2)) by SERIES_1:8
.= Partial_Sums (Im (seq1 + seq2)) by Th15
.= Im (Partial_Sums (seq1 + seq2)) by Th26 ;
Re ((Partial_Sums seq1) + (Partial_Sums seq2)) = (Re (Partial_Sums seq1)) + (Re (Partial_Sums seq2)) by Th15
.= (Partial_Sums (Re seq1)) + (Re (Partial_Sums seq2)) by Th26
.= (Partial_Sums (Re seq1)) + (Partial_Sums (Re seq2)) by Th26
.= Partial_Sums ((Re seq1) + (Re seq2)) by SERIES_1:8
.= Partial_Sums (Re (seq1 + seq2)) by Th15
.= Re (Partial_Sums (seq1 + seq2)) by Th26 ;
hence (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by A1, Th14; :: thesis: verum