theorem Th23: :: LOPBAN_4:23

for X being Banach_Algebra
for w, z being Element of X
for k being Nat holds (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k)