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