let th be Real; :: thesis: (exp (th * <i>)) *' = exp (- (th * <i>))
(exp (th * <i>)) *' = (Sum ((th * <i>) ExpSeq)) *' by Def14
.= Sum ((- (th * <i>)) ExpSeq) by Lm4
.= exp (- (th * <i>)) by Def14 ;
hence (exp (th * <i>)) *' = exp (- (th * <i>)) ; :: thesis: verum