theorem Th13: :: SIN_COS2:13

exp_R . 0 = 1 by SIN_COS:51, SIN_COS:def 23;