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