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) )
(- 1) (#) f = - f ;
hence - f is_right_convergent_in x0 by A1, Th60; :: thesis: lim_right (- f),x0 = - (lim_right f,x0)
thus lim_right (- f),x0 = (- 1) * (lim_right f,x0) by A1, Th60
.= - (lim_right f,x0) ; :: thesis: verum