theorem Th25: :: LOPBAN_4:25

for X being Banach_Algebra
for n being Nat
for z, w being Element of X st z,w are_commutative holds
(Partial_Sums ((z + w) rExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n