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