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: now :: thesis: for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom (f1 + f2) holds
( (f1 + f2) /* seq is convergent & lim ((f1 + f2) /* seq) = (lim_in-infty f1) + (lim_in-infty f2) )

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) ) )
assume that
A5: seq is divergent_to-infty and
A6: rng seq c= dom (f1 + f2) ; :: thesis: ( (f1 + f2) /* seq is convergent & lim ((f1 + f2) /* seq) = (lim_in-infty f1) + (lim_in-infty f2) )
A7: rng seq c= (dom f1) /\ (dom f2) by A6, VALUED_1:def 1;
(dom f1) /\ (dom f2) c= dom f2 by XBOOLE_1:17;
then A8: rng seq c= dom f2 by A7;
then A9: lim (f2 /* seq) = lim_in-infty f2 by A2, A5, Def13;
A10: f2 /* seq is convergent by A2, A5, A8;
(dom f1) /\ (dom f2) c= dom f1 by XBOOLE_1:17;
then A11: rng seq c= dom f1 by A7;
then A12: lim (f1 /* seq) = lim_in-infty f1 by A1, A5, Def13;
A13: f1 /* seq is convergent by A1, A5, A11;
then (f1 /* seq) + (f2 /* seq) is convergent by A10;
hence (f1 + f2) /* seq is convergent by A7, RFUNCT_2:8; :: thesis: lim ((f1 + f2) /* seq) = (lim_in-infty f1) + (lim_in-infty f2)
thus lim ((f1 + f2) /* seq) = lim ((f1 /* seq) + (f2 /* seq)) by A7, RFUNCT_2:8
.= (lim_in-infty f1) + (lim_in-infty f2) by A13, A12, A10, A9, SEQ_2:6 ; :: thesis: verum

end;

hence f1 + f2 is convergent_in-infty by A3; :: 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 A4, Def13; :: thesis: verum