theorem Th17: :: SIN_COS:17

for z being Complex holds 1 <= Sum (|.z.| rExpSeq)