let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is convergent_in-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 - f2) ) ) implies ( f1 - f2 is convergent_in-infty & lim_in-infty (f1 - f2) = (lim_in-infty f1) - (lim_in-infty f2) ) )
assume that
A1: f1 is convergent_in-infty and
A2: f2 is convergent_in-infty and
A3: for r being Real ex g being Real st
( g < r & g in dom (f1 - f2) ) ; :: thesis: ( f1 - f2 is convergent_in-infty & lim_in-infty (f1 - f2) = (lim_in-infty f1) - (lim_in-infty f2) )
A4: - f2 is convergent_in-infty by A2, Th90;
hence f1 - f2 is convergent_in-infty by A1, A3, Th91; :: thesis: lim_in-infty (f1 - f2) = (lim_in-infty f1) - (lim_in-infty f2)
lim_in-infty (- f2) = - (lim_in-infty f2) by A2, Th90;
hence lim_in-infty (f1 - f2) = (lim_in-infty f1) + (- (lim_in-infty f2)) by A1, A3, A4, Th91
.= (lim_in-infty f1) - (lim_in-infty f2) ;
:: thesis: verum