for w, z being Complex
for k, n being Nat holds |.((Partial_Sums |.(Conj (k,z,w)).|) . n).| = (Partial_Sums |.(Conj (k,z,w)).|) . n