let X be Complex_Banach_Algebra; :: thesis: for z, w being Element of X st z,w are_commutative holds
(Sum (z ExpSeq )) * (Sum (w ExpSeq )) = Sum ((z + w) ExpSeq )
let z, w be Element of X; :: thesis: ( z,w are_commutative implies (Sum (z ExpSeq )) * (Sum (w ExpSeq )) = Sum ((z + w) ExpSeq ) )
assume A1: z,w are_commutative ; :: thesis: (Sum (z ExpSeq )) * (Sum (w ExpSeq )) = Sum ((z + w) ExpSeq )
deffunc H₁( Element of NAT ) -> Element of the carrier of X = (Partial_Sums (Conj $1,z,w)) . $1;
ex seq being sequence of X st
for k being Element of NAT holds seq . k = H₁(k) from FUNCT_2:sch 4();
then consider seq being sequence of X 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 A1, Th25
.= (((Partial_Sums (z ExpSeq )) * (Partial_Sums (w ExpSeq ))) . k) - ((Partial_Sums ((z + w) ExpSeq )) . k) by CLOPBAN3:def 10
.= (((Partial_Sums (z ExpSeq )) * (Partial_Sums (w ExpSeq ))) - (Partial_Sums ((z + w) ExpSeq ))) . k by NORMSP_1:def 6 ; :: thesis: verum

end;

then A3: seq = ((Partial_Sums (z ExpSeq )) * (Partial_Sums (w ExpSeq ))) - (Partial_Sums ((z + w) ExpSeq )) by FUNCT_2:113;
A4: Partial_Sums (z ExpSeq ) is convergent by CLOPBAN3:def 2;
A5: Partial_Sums (w ExpSeq ) is convergent by CLOPBAN3:def 2;
A6: Partial_Sums ((z + w) ExpSeq ) is convergent by CLOPBAN3:def 2;
A7: ( (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 A4, A5, Th3, Th8;
A8: ( seq is convergent & lim seq = 0. X ) by A2, Th32;
thus Sum ((z + w) ExpSeq ) = lim (Partial_Sums ((z + w) ExpSeq )) by CLOPBAN3:def 3
.= (lim (Partial_Sums (z ExpSeq ))) * (lim (Partial_Sums (w ExpSeq ))) by A3, A6, A7, A8, Th1
.= (Sum (z ExpSeq )) * (lim (Partial_Sums (w ExpSeq ))) by CLOPBAN3:def 3
.= (Sum (z ExpSeq )) * (Sum (w ExpSeq )) by CLOPBAN3:def 3 ; :: thesis: verum