theorem :: SIN_COS:51

exp_R 0 = 1 by Lm11;