theorem Th21: :: SIN_COS:21

for w, z being Complex
for p being Real st p > 0 holds
ex n being Nat st
for k being Nat st n <= k holds
|.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < p