let w, z be Complex; 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
A2:
( (Partial_Sums |.(Conj (k,z,w)).|) . 0 <= (Partial_Sums |.(Conj (k,z,w)).|) . n & (Partial_Sums |.(Conj (k,z,w)).|) . 0 = |.(Conj (k,z,w)).| . 0 )
by SEQM_3:6, 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, ABSVALUE:def 1; verum