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 A1: ( 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) ) ) ) ; :: thesis: ( f1 + f2 is convergent_in-infty & lim_in-infty (f1 + f2) = (lim_in-infty f1) + (lim_in-infty f2) )

A2: now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to-infty & rng seq c= dom (f1 + f2) implies ( (f1 + f2) /* seq is convergent & lim ((f1 + f2) /* seq) = (lim_in-infty f1) + (lim_in-infty f2) ) )
A3: ( lim_in-infty f1 = lim_in-infty f1 & lim_in-infty f2 = lim_in-infty f2 ) ;
assume A4: ( seq is divergent_to-infty & rng seq c= dom (f1 + f2) ) ; :: thesis: ( (f1 + f2) /* seq is convergent & lim ((f1 + f2) /* seq) = (lim_in-infty f1) + (lim_in-infty f2) )
then A5: rng seq c= (dom f1) /\ (dom f2) by VALUED_1:def 1;
( (dom f1) /\ (dom f2) c= dom f1 & (dom f1) /\ (dom f2) c= dom f2 ) by XBOOLE_1:17;
then A6: ( rng seq c= dom f1 & rng seq c= dom f2 ) by A5, XBOOLE_1:1;
then A7: ( f1 /* seq is convergent & lim (f1 /* seq) = lim_in-infty f1 ) by A1, A3, A4, Def13;
A8: ( f2 /* seq is convergent & lim (f2 /* seq) = lim_in-infty f2 ) by A1, A3, A4, A6, Def13;
then (f1 /* seq) + (f2 /* seq) is convergent by A7, SEQ_2:19;
hence (f1 + f2) /* seq is convergent by A5, RFUNCT_2:23; :: thesis: lim ((f1 + f2) /* seq) = (lim_in-infty f1) + (lim_in-infty f2)
thus lim ((f1 + f2) /* seq) = lim ((f1 /* seq) + (f2 /* seq)) by A5, RFUNCT_2:23
.= (lim_in-infty f1) + (lim_in-infty f2) by A7, A8, SEQ_2:20 ; :: thesis: verum

end;

hence f1 + f2 is convergent_in-infty by A1, Def9; :: thesis: lim_in-infty (f1 + f2) = (lim_in-infty f1) + (lim_in-infty f2)
hence lim_in-infty (f1 + f2) = (lim_in-infty f1) + (lim_in-infty f2) by A2, Def13; :: thesis: verum