let X be Complex_Banach_Algebra; :: thesis: for z, w being Element of X
for k, n being Element of NAT holds abs ((Partial_Sums ||.(Conj k,z,w).||) . n) = (Partial_Sums ||.(Conj k,z,w).||) . n
let z, w be Element of X; :: thesis: for k, n being Element of NAT holds abs ((Partial_Sums ||.(Conj k,z,w).||) . n) = (Partial_Sums ||.(Conj k,z,w).||) . n
let k, n be Element of NAT ; :: thesis: abs ((Partial_Sums ||.(Conj k,z,w).||) . n) = (Partial_Sums ||.(Conj k,z,w).||) . n

A1: now

let n be Element of NAT ; :: thesis: 0 <= ||.(Conj k,z,w).|| . n
||.(Conj k,z,w).|| . n = ||.((Conj k,z,w) . n).|| by CLVECT_1:def 17;
hence 0 <= ||.(Conj k,z,w).|| . n by CLVECT_1:106; :: thesis: verum

end;

then A2: Partial_Sums ||.(Conj k,z,w).|| is non-decreasing by SERIES_1:19;
0 <= n by NAT_1:2;
then A3: (Partial_Sums ||.(Conj k,z,w).||) . 0 <= (Partial_Sums ||.(Conj k,z,w).||) . n by A2, SEQM_3:12;
A4: (Partial_Sums ||.(Conj k,z,w).||) . 0 = ||.(Conj k,z,w).|| . 0 by SERIES_1:def 1;
0 <= ||.(Conj k,z,w).|| . 0 by A1;
hence abs ((Partial_Sums ||.(Conj k,z,w).||) . n) = (Partial_Sums ||.(Conj k,z,w).||) . n by A3, A4, ABSVALUE:def 1; :: thesis: verum