theorem :: SIN_COS:26

for th being Real holds (exp (th * <i>)) *' = exp (- (th * <i>))