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 COMSEQ_3:def 7
.= (((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:118
.= ((Partial_Sums seq) . (n + 1)) *' by COMSEQ_3:def 7 ;
hence S₁[n + 1] by COMSEQ_2:def 2; :: thesis: verum

end;

(Partial_Sums (seq *' )) . 0 = (seq *' ) . 0 by COMSEQ_3:def 7
.= (seq . 0 ) *' by COMSEQ_2:def 2
.= ((Partial_Sums seq) . 0 ) *' by COMSEQ_3:def 7 ;
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:113; :: thesis: verum