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
( r < g & 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
( r < g & 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, Th81;
hence f1 - f2 is convergent_in+infty by A1, A3, Th82; :: thesis: lim_in+infty (f1 - f2) = (lim_in+infty f1) - (lim_in+infty f2)
lim_in+infty (- f2) = - (lim_in+infty f2) by A2, Th81;
hence lim_in+infty (f1 - f2) = (lim_in+infty f1) + (- (lim_in+infty f2)) by A1, A3, A4, Th82
.= (lim_in+infty f1) - (lim_in+infty f2) ;
:: thesis: verum