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