let seq be Complex_Sequence; :: thesis: Partial_Sums (seq *') = (Partial_Sums seq) *'
defpred S1[ Nat] means (Partial_Sums (seq *')) . \$1 = ((Partial_Sums seq) *') . \$1;
A1: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
A2: n in NAT by ORDINAL1:def 12;
assume A3: S1[n] ; :: thesis: S1[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
.= (((Partial_Sums seq) . n) *') + ((seq . (n + 1)) *') by
.= (((Partial_Sums seq) . n) + (seq . (n + 1))) *' by COMPLEX1:32
.= ((Partial_Sums seq) . (n + 1)) *' by SERIES_1:def 1 ;
hence S1[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: S1[ 0 ] by COMSEQ_2:def 2;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A1);
then for n being Element of NAT holds S1[n] ;
hence Partial_Sums (seq *') = (Partial_Sums seq) *' by FUNCT_2:63; :: thesis: verum