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 Th18
.= (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:6
.= Partial_Sums (Im (seq1 - seq2)) by Th18
.= Im (Partial_Sums (seq1 - seq2)) by Th26 ;
Re ((Partial_Sums seq1) - (Partial_Sums seq2)) = (Re (Partial_Sums seq1)) - (Re (Partial_Sums seq2)) by Th18
.= (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:6
.= Partial_Sums (Re (seq1 - seq2)) by Th18
.= Re (Partial_Sums (seq1 - seq2)) by Th26 ;
hence (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by A1, Th14; :: thesis: verum