let X be Complex_Banach_Algebra; 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; 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; |.((Partial_Sums ||.(Conj (k,z,w)).||) . n).| = (Partial_Sums ||.(Conj (k,z,w)).||) . n
then
Partial_Sums ||.(Conj (k,z,w)).|| is non-decreasing
by SERIES_1:16;
then A2:
(Partial_Sums ||.(Conj (k,z,w)).||) . 0 <= (Partial_Sums ||.(Conj (k,z,w)).||) . n
by SEQM_3:6;
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
|.((Partial_Sums ||.(Conj (k,z,w)).||) . n).| = (Partial_Sums ||.(Conj (k,z,w)).||) . n
by A2, A3, ABSVALUE:def 1; verum