let seq be Complex_Sequence; :: thesis: Partial_Sums (seq *') = (Partial_Sums seq) *'
defpred S₁[ Nat] means (Partial_Sums (seq *')) . $1 = ((Partial_Sums seq) *') . $1;

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
A2: n in NAT by ORDINAL1:def 12;
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
(Partial_Sums (seq *')) . (n + 1) = ((Partial_Sums (seq *')) . n) + ((seq *') . (n + 1)) by SERIES_1:def 1
.= (((Partial_Sums seq) *') . n) + ((seq . (n + 1)) *') by A3, COMSEQ_2:def 2
.= (((Partial_Sums seq) . n) *') + ((seq . (n + 1)) *') by COMSEQ_2:def 2, A2
.= (((Partial_Sums seq) . n) + (seq . (n + 1))) *' by COMPLEX1:32
.= ((Partial_Sums seq) . (n + 1)) *' by SERIES_1:def 1 ;
hence S₁[n + 1] by COMSEQ_2:def 2; :: thesis: verum

end;

(Partial_Sums (seq *')) . 0 = (seq *') . 0 by SERIES_1:def 1
.= (seq . 0) *' by COMSEQ_2:def 2
.= ((Partial_Sums seq) . 0) *' by SERIES_1:def 1 ;
then A4: S₁[ 0 ] by COMSEQ_2:def 2;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
then for n being Element of NAT holds S₁[n] ;
hence Partial_Sums (seq *') = (Partial_Sums seq) *' by FUNCT_2:63; :: thesis: verum