theorem Th26: :: LOPBAN_4:26

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