let w, z be Complex; :: 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: 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 VALUED_1:18;
hence 0 <= |.(Conj (k,z,w)).| . n by COMPLEX1:46; :: thesis: verum
end;
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; :: thesis: verum