theorem Th18: :: SIN_COS:18

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