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

end;

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