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: 0 <= n by NAT_1:2;

A2: 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 NORMSP_0:def 4;
hence 0 <= ||.(Conj (k,z,w)).|| . n by CLVECT_1:106; :: thesis: verum

end;

then Partial_Sums ||.(Conj (k,z,w)).|| is non-decreasing by SERIES_1:19;
then A3: (Partial_Sums ||.(Conj (k,z,w)).||) . 0 <= (Partial_Sums ||.(Conj (k,z,w)).||) . n by A1, 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 A2;
hence abs ((Partial_Sums ||.(Conj (k,z,w)).||) . n) = (Partial_Sums ||.(Conj (k,z,w)).||) . n by A3, A4, ABSVALUE:def 1; :: thesis: verum