let X be Complex_Banach_Algebra; :: thesis: for z being Element of X
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 z be Element of X; :: 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 Th26;
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