theorem Th16: :: CLOPBAN4:16
for X being Complex_Banach_Algebra
for n being Nat
for z, w being Element of X st z,w are_commutative holds
(z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n