let z be Complex; :: thesis: 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) ) )
let m, n be Nat; :: thesis: ( |.((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) ) )
for n being Nat holds 0 <= (|.z.| rExpSeq) . n by Th18;
hence ( |.((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) ) ) by COMSEQ_3:9; :: thesis: verum