theorem Th12: :: SIN_COS:12

for w, z being Complex
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)