theorem Th19: :: LOPBAN_4:19
for X being Banach_Algebra
for n being Nat
for z, w being Element of X st z,w are_commutative holds
(1 / (n !)) * ((z + w) #N n) = (Partial_Sums (Expan_e (n,z,w))) . n