for n being Nat
for z being Complex holds
( (z ExpSeq) . (n + 1) = (((z ExpSeq) . n) * z) / ((n + 1) + (0 * <i>)) & (z ExpSeq) . 0 = 1 & |.((z ExpSeq) . n).| = (|.z.| rExpSeq) . n )