let X be Complex_Banach_Algebra; :: thesis: for z, w being Element of X st z,w are_commutative holds
(Sum ()) * (Sum ()) = Sum ((z + w) ExpSeq)

let z, w be Element of X; :: thesis: ( z,w are_commutative implies (Sum ()) * (Sum ()) = Sum ((z + w) ExpSeq) )
assume A1: z,w are_commutative ; :: thesis: (Sum ()) * (Sum ()) = Sum ((z + w) ExpSeq)
deffunc H1( 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 = H1(k) from 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 ;
A3: for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k
proof
let k be Nat; :: thesis: seq . k = (Partial_Sums (Conj (k,z,w))) . k
k in NAT by ORDINAL1:def 12;
hence seq . k = (Partial_Sums (Conj (k,z,w))) . k by A2; :: thesis: verum
end;
now :: thesis: for k being Element of NAT holds seq . k = ((() * ()) - (Partial_Sums ((z + w) ExpSeq))) . k
let k be Element of NAT ; :: thesis: seq . k = ((() * ()) - (Partial_Sums ((z + w) ExpSeq))) . k
thus seq . k = (Partial_Sums (Conj (k,z,w))) . k by A2
.= ((() . k) * (() . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) by
.= ((() * ()) . k) - ((Partial_Sums ((z + w) ExpSeq)) . k) by LOPBAN_3:def 7
.= ((() * ()) - (Partial_Sums ((z + w) ExpSeq))) . k by NORMSP_1:def 3 ; :: thesis: verum
end;
then A4: seq = (() * ()) - (Partial_Sums ((z + w) ExpSeq)) by FUNCT_2:63;
A5: Partial_Sums () is convergent by CLOPBAN3:def 1;
A6: lim seq = 0. X by ;
A7: Partial_Sums ((z + w) ExpSeq) is convergent by CLOPBAN3:def 1;
A8: Partial_Sums () is convergent by CLOPBAN3:def 1;
then A9: (Partial_Sums ()) * () is convergent by ;
A10: lim (() * ()) = (lim ()) * (lim ()) by A8, A5, Th8;
thus Sum ((z + w) ExpSeq) = lim (Partial_Sums ((z + w) ExpSeq)) by CLOPBAN3:def 2
.= (lim ()) * (lim ()) by A4, A7, A9, A10, A6, Th1
.= (Sum ()) * (lim ()) by CLOPBAN3:def 2
.= (Sum ()) * (Sum ()) by CLOPBAN3:def 2 ; :: thesis: verum