theorem Th16: :: SIN_COS:16

for z being Complex
for k being Nat holds
( |.((Partial_Sums (z ExpSeq)) . k).| <= (Partial_Sums (|.z.| rExpSeq)) . k & (Partial_Sums (|.z.| rExpSeq)) . k <= Sum (|.z.| rExpSeq) & |.((Partial_Sums (z ExpSeq)) . k).| <= Sum (|.z.| rExpSeq) )