:: deftheorem defines exp_R SIN_COS:def 23 :
for th being Real holds exp_R th = exp_R . th;