let f be PartFunc of REAL ,REAL ; :: thesis: ( f is convergent_in+infty implies ( - f is convergent_in+infty & lim_in+infty (- f) = - (lim_in+infty f) ) )
assume A1: f is convergent_in+infty ; :: thesis: ( - f is convergent_in+infty & lim_in+infty (- f) = - (lim_in+infty f) )
(- 1) (#) f = - f ;
hence - f is convergent_in+infty by A1, Th115; :: thesis: lim_in+infty (- f) = - (lim_in+infty f)
thus lim_in+infty (- f) = (- 1) * (lim_in+infty f) by A1, Th115
.= - (lim_in+infty f) ; :: thesis: verum