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

A1: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: 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 A2, COMSEQ_2:def 2
.= (((Partial_Sums seq) . n) *') + ((seq . (n + 1)) *') by COMSEQ_2:def 2
.= (((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 A3: S₁[ 0 ] by COMSEQ_2:def 2;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A1);
hence Partial_Sums (seq *') = (Partial_Sums seq) *' by FUNCT_2:63; :: thesis: verum