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