let z0, w0 be Complex; :: thesis: (Sum (z0 ExpSeq)) * (Sum (w0 ExpSeq)) = Sum ((z0 + w0) ExpSeq)
reconsider z = z0, w = w0 as Element of COMPLEX by XCMPLX_0:def 2;
deffunc H₁( Nat) -> Element of COMPLEX = (Partial_Sums (Conj ($1,z,w))) . $1;
ex seq being Complex_Sequence st
for k being Nat holds seq . k = H₁(k) from COMSEQ_1:sch 1();
then consider seq being Complex_Sequence such that
A1: for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ;
then A2: seq = ((Partial_Sums (z ExpSeq)) (#) (Partial_Sums (w ExpSeq))) - (Partial_Sums ((z + w) ExpSeq)) ;
A3: ( (Partial_Sums (z ExpSeq)) (#) (Partial_Sums (w ExpSeq)) is convergent & lim ((Partial_Sums (z ExpSeq)) (#) (Partial_Sums (w ExpSeq))) = (lim (Partial_Sums (z ExpSeq))) * (lim (Partial_Sums (w ExpSeq))) ) by COMSEQ_2:30;
lim seq = 0c by A1, Th22;
hence (Sum (z0 ExpSeq)) * (Sum (w0 ExpSeq)) = Sum ((z0 + w0) ExpSeq) by A2, A3, COMSEQ_3:10; :: thesis: verum