let X be Banach_Algebra; :: thesis: for w, z being Element of X
for k, n being Nat holds |.((Partial_Sums ||.(Conj (k,z,w)).||) . n).| = (Partial_Sums ||.(Conj (k,z,w)).||) . n
let w, z be Element of X; :: thesis: for k, n being Nat holds |.((Partial_Sums ||.(Conj (k,z,w)).||) . n).| = (Partial_Sums ||.(Conj (k,z,w)).||) . n
let k, n be Nat; :: thesis: |.((Partial_Sums ||.(Conj (k,z,w)).||) . n).| = (Partial_Sums ||.(Conj (k,z,w)).||) . n
A1: (Partial_Sums ||.(Conj (k,z,w)).||) . 0 = ||.(Conj (k,z,w)).|| . 0 by SERIES_1:def 1;
A2: now :: thesis: for n being Nat holds 0 <= ||.(Conj (k,z,w)).|| . n
let n be 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 NORMSP_1:4; :: thesis: verum
end;
then Partial_Sums ||.(Conj (k,z,w)).|| is non-decreasing by SERIES_1:16;
then A3: (Partial_Sums ||.(Conj (k,z,w)).||) . 0 <= (Partial_Sums ||.(Conj (k,z,w)).||) . n by SEQM_3:6;
0 <= ||.(Conj (k,z,w)).|| . 0 by A2;
hence |.((Partial_Sums ||.(Conj (k,z,w)).||) . n).| = (Partial_Sums ||.(Conj (k,z,w)).||) . n by A3, A1, ABSVALUE:def 1; :: thesis: verum