theorem Th57: :: SIN_COS:58

for p being Real st p > 0 holds
ex q being Real st
( q > 0 & ( for z being Complex st |.z.| < q holds
|.(Sum (z P_dt)).| < p ) )