let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds
( - f is_right_convergent_in x0 & lim_right ((- f),x0) = - (lim_right (f,x0)) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_right_convergent_in x0 implies ( - f is_right_convergent_in x0 & lim_right ((- f),x0) = - (lim_right (f,x0)) ) )
assume A1: f is_right_convergent_in x0 ; :: thesis: ( - f is_right_convergent_in x0 & lim_right ((- f),x0) = - (lim_right (f,x0)) )
thus - f is_right_convergent_in x0 by A1, Th52; :: thesis: lim_right ((- f),x0) = - (lim_right (f,x0))
thus lim_right ((- f),x0) = (- 1) * (lim_right (f,x0)) by A1, Th52
.= - (lim_right (f,x0)) ; :: thesis: verum