set X = dom (f1 + f2);
dom (f1 + f2) c= (dom f1) /\ (dom f2) by VALUED_1:def 1;
then X: ( dom (f1 + f2) c= dom f1 & dom (f1 + f2) c= dom f2 ) by XBOOLE_1:18;
HA: ( f1 | (dom (f1 + f2)) is continuous & f2 | (dom (f1 + f2)) is continuous ) ;

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 in dom (f1 + f2) implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) ) )
assume A8: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 in dom (f1 + f2) ) ; :: thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) )
then A9: rng s1 c= (dom f1) /\ (dom f2) by VALUED_1:def 1;
A10: ( f1 /* s1 is convergent & f1 . (lim s1) = lim (f1 /* s1) ) by A8, Th14, X, HA;
A11: ( f2 /* s1 is convergent & f2 . (lim s1) = lim (f2 /* s1) ) by A8, Th14, X, HA;
then A12: (f1 /* s1) + (f2 /* s1) is convergent by A10, SEQ_2:19;
(f1 + f2) . (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A8, A10, A11, VALUED_1:def 1
.= lim ((f1 /* s1) + (f2 /* s1)) by A10, A11, SEQ_2:20
.= lim ((f1 + f2) /* s1) by A9, RFUNCT_2:23 ;
hence ( (f1 + f2) /* s1 is convergent & (f1 + f2) . (lim s1) = lim ((f1 + f2) /* s1) ) by A9, A12, RFUNCT_2:23; :: thesis: verum

end;

then (f1 + f2) | (dom (f1 + f2)) is continuous by Th14;
hence for b₁ being PartFunc of REAL ,REAL st b₁ = f1 + f2 holds
b₁ is continuous by RELAT_1:98; :: thesis: verum