let seq1, seq be Complex_Sequence; :: thesis: ( ( for n being Element of NAT holds seq1 . n = seq . 0 ) implies Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 )
assume A1: for n being Element of NAT holds seq1 . n = seq . 0 ; :: thesis: Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1

A2: now

let n be Element of NAT ; :: thesis: ( (Re seq1) . n = (Re seq) . 0 & (Im seq1) . n = (Im seq) . 0 )
thus (Re seq1) . n = Re (seq1 . n) by Def3
.= Re (seq . 0 ) by A1
.= (Re seq) . 0 by Def3 ; :: thesis: (Im seq1) . n = (Im seq) . 0
thus (Im seq1) . n = Im (seq1 . n) by Def4
.= Im (seq . 0 ) by A1
.= (Im seq) . 0 by Def4 ; :: thesis: verum

end;

A3: Re (Partial_Sums (seq ^\ 1)) = Partial_Sums (Re (seq ^\ 1)) by Th26
.= Partial_Sums ((Re seq) ^\ 1) by Th23
.= ((Partial_Sums (Re seq)) ^\ 1) - (Re seq1) by A2, SERIES_1:14
.= (Re ((Partial_Sums seq) ^\ 1)) - (Re seq1) by Th32
.= Re (((Partial_Sums seq) ^\ 1) - seq1) by Th18 ;
Im (Partial_Sums (seq ^\ 1)) = Partial_Sums (Im (seq ^\ 1)) by Th26
.= Partial_Sums ((Im seq) ^\ 1) by Th23
.= ((Partial_Sums (Im seq)) ^\ 1) - (Im seq1) by A2, SERIES_1:14
.= (Im ((Partial_Sums seq) ^\ 1)) - (Im seq1) by Th32
.= Im (((Partial_Sums seq) ^\ 1) - seq1) by Th18 ;
hence Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 by A3, Th14; :: thesis: verum