theorem Th19: :: SIN_COS:19

for z being Complex
for m, n being Nat holds
( |.((Partial_Sums (|.z.| rExpSeq)) . n).| = (Partial_Sums (|.z.| rExpSeq)) . n & ( n <= m implies |.(((Partial_Sums (|.z.| rExpSeq)) . m) - ((Partial_Sums (|.z.| rExpSeq)) . n)).| = ((Partial_Sums (|.z.| rExpSeq)) . m) - ((Partial_Sums (|.z.| rExpSeq)) . n) ) )