for z being Complex
for n being Nat holds 0 <= (|.z.| rExpSeq) . n