for x being Real holds sin_C /. x = sin . x