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, Th124; :: thesis: lim_in-infty (- f) = - (lim_in-infty f)
thus lim_in-infty (- f) = (- 1) * (lim_in-infty f) by A1, Th124
.= - (lim_in-infty f) ; :: thesis: verum