theorem Th13: :: SIN_COS:13

for w, z being Complex
for k being Nat holds (z ExpSeq) . k = (Expan_e (k,z,w)) . k