let X be 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 NORMSP_1:def 10;
hence 0 <= ||.(Conj k,z,w).|| . n by NORMSP_1:8; :: thesis: verum

end;

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