theorem Th14: :: SIN_COS:14
for w, z being Complex
for n being Nat holds (Partial_Sums ((z + w) ExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n