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