theorem Th36: :: SIN_COS:37
for th being Real holds
( cos . th = Sum (th P_cos) & sin . th = Sum (th P_sin) )