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