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