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) ) )
A1: for n being Element of NAT holds 0 <= (|.z.| rExpSeq ) . n by Th19;
thus ( 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 A1, COMSEQ_3:9; :: thesis: verum