for w, z being Complex
for seq being Complex_Sequence st ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds
( seq is convergent & lim seq = 0 )