theorem Th25: :: CLOPBAN4:25

for X being Complex_Banach_Algebra
for k being Nat
for z, w being Element of X st z,w are_commutative holds
(((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k