let f, g be PartFunc of REAL,REAL; :: thesis: ( f is continuous & not f is empty & g is continuous & not g is empty & ex a, b, c being Real st
( dom f = [.a,b.] & dom g = [.b,c.] ) & f tolerates g implies f +* g is continuous )
assume ( f is continuous & not f is empty & g is continuous & not g is empty & ex a, b, c being Real st
( dom f = [.a,b.] & dom g = [.b,c.] ) & f tolerates g ) ; :: thesis: f +* g is continuous
then consider h being PartFunc of REAL,REAL such that
A2: ( h = f +* g & ( for x being Real st x in dom h holds
h is_continuous_in x ) ) by LemGlue;
thus f +* g is continuous by A2; :: thesis: verum