theorem Th39: :: SIN_COS3:39

for x being Real holds cos_C /. x = cos . x