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: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 abs ((Partial_Sums |.(Conj (k,z,w)).|) . n) = (Partial_Sums |.(Conj (k,z,w)).|) . n by A2, ABSVALUE:def 1; :: thesis: verum