let seq be Complex_Sequence; :: thesis: Partial_Sums (seq *') = (Partial_Sums seq) *'

defpred S_{1}[ Nat] means (Partial_Sums (seq *')) . $1 = ((Partial_Sums seq) *') . $1;

.= (seq . 0) *' by COMSEQ_2:def 2

.= ((Partial_Sums seq) . 0) *' by SERIES_1:def 1 ;

then A4: S_{1}[ 0 ]
by COMSEQ_2:def 2;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A1);

then for n being Element of NAT holds S_{1}[n]
;

hence Partial_Sums (seq *') = (Partial_Sums seq) *' by FUNCT_2:63; :: thesis: verum

defpred S

A1: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

(Partial_Sums (seq *')) . 0 =
(seq *') . 0
by SERIES_1:def 1
S

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

A2: n in NAT by ORDINAL1:def 12;

assume A3: S_{1}[n]
; :: thesis: S_{1}[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_{1}[n + 1]
by COMSEQ_2:def 2; :: thesis: verum

end;A2: n in NAT by ORDINAL1:def 12;

assume A3: S

(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

.= (seq . 0) *' by COMSEQ_2:def 2

.= ((Partial_Sums seq) . 0) *' by SERIES_1:def 1 ;

then A4: S

for n being Nat holds S

then for n being Element of NAT holds S

hence Partial_Sums (seq *') = (Partial_Sums seq) *' by FUNCT_2:63; :: thesis: verum