let z be Element of COMPLEX ; :: thesis: for n, m being Element of NAT holds
( abs ((Partial_Sums (|.z.| rExpSeq )) . n) = (Partial_Sums (|.z.| rExpSeq )) . n & ( n <= m implies abs (((Partial_Sums (|.z.| rExpSeq )) . m) - ((Partial_Sums (|.z.| rExpSeq )) . n)) = ((Partial_Sums (|.z.| rExpSeq )) . m) - ((Partial_Sums (|.z.| rExpSeq )) . n) ) )
let n, m be Element of NAT ; :: thesis: ( abs ((Partial_Sums (|.z.| rExpSeq )) . n) = (Partial_Sums (|.z.| rExpSeq )) . n & ( n <= m implies abs (((Partial_Sums (|.z.| rExpSeq )) . m) - ((Partial_Sums (|.z.| rExpSeq )) . n)) = ((Partial_Sums (|.z.| rExpSeq )) . m) - ((Partial_Sums (|.z.| rExpSeq )) . n) ) )
for n being Element of NAT holds 0 <= (|.z.| rExpSeq ) . n by Th19;
hence ( abs ((Partial_Sums (|.z.| rExpSeq )) . n) = (Partial_Sums (|.z.| rExpSeq )) . n & ( n <= m implies abs (((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