let z0, w0 be complex number ; :: 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₁( Element of NAT ) -> Element of COMPLEX = (Partial_Sums (Conj $1,z,w)) . $1;
ex seq being Complex_Sequence st
for k being Element of NAT holds seq . k = H₁(k) from COMSEQ_1:sch 1();
then consider seq being Complex_Sequence such that
A2: for k being Element of NAT holds seq . k = (Partial_Sums (Conj k,z,w)) . k ;

now

let k be Element of NAT ; :: thesis: seq . k = (((Partial_Sums (z ExpSeq )) (#) (Partial_Sums (w ExpSeq ))) - (Partial_Sums ((z + w) ExpSeq ))) . k
thus seq . k = (Partial_Sums (Conj k,z,w)) . k by A2
.= (((Partial_Sums (z ExpSeq )) . k) * ((Partial_Sums (w ExpSeq )) . k)) - ((Partial_Sums ((z + w) ExpSeq )) . k) by Th16
.= (((Partial_Sums (z ExpSeq )) (#) (Partial_Sums (w ExpSeq ))) . k) - ((Partial_Sums ((z + w) ExpSeq )) . k) by VALUED_1:5
.= (((Partial_Sums (z ExpSeq )) (#) (Partial_Sums (w ExpSeq ))) . k) + ((- (Partial_Sums ((z + w) ExpSeq ))) . k) by VALUED_1:8
.= (((Partial_Sums (z ExpSeq )) (#) (Partial_Sums (w ExpSeq ))) - (Partial_Sums ((z + w) ExpSeq ))) . k by VALUED_1:1 ; :: thesis: verum

end;

then A4: seq = ((Partial_Sums (z ExpSeq )) (#) (Partial_Sums (w ExpSeq ))) - (Partial_Sums ((z + w) ExpSeq )) by FUNCT_2:113;
A5: ( (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:29, COMSEQ_2:30;
lim seq = 0c by A2, Th23;
hence (Sum (z0 ExpSeq )) * (Sum (w0 ExpSeq )) = Sum ((z0 + w0) ExpSeq ) by A4, A5, COMSEQ_3:10; :: thesis: verum