let seq, seq1 be Complex_Sequence; :: thesis: ( ( for n being Nat holds seq1 . n = seq . 0 ) implies Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 )
assume A1: for n being Nat holds seq1 . n = seq . 0 ; :: thesis: Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
A2: now :: thesis: for n being Nat holds
( (Re seq1) . n = (Re seq) . 0 & (Im seq1) . n = (Im seq) . 0 )
let n be Nat; :: thesis: ( (Re seq1) . n = (Re seq) . 0 & (Im seq1) . n = (Im seq) . 0 )
thus (Re seq1) . n = Re (seq1 . n) by Def5
.= Re (seq . 0) by A1
.= (Re seq) . 0 by Def5 ; :: thesis: (Im seq1) . n = (Im seq) . 0
thus (Im seq1) . n = Im (seq1 . n) by Def6
.= Im (seq . 0) by A1
.= (Im seq) . 0 by Def6 ; :: thesis: verum
end;
A3: 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:11
.= (Im ((Partial_Sums seq) ^\ 1)) - (Im seq1) by Th32
.= Im (((Partial_Sums seq) ^\ 1) - seq1) by Th18 ;
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:11
.= (Re ((Partial_Sums seq) ^\ 1)) - (Re seq1) by Th32
.= Re (((Partial_Sums seq) ^\ 1) - seq1) by Th18 ;
hence Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 by A3, Th14; :: thesis: verum