let a, b be Real; :: thesis: for f, g being PartFunc of REAL,REAL st g is continuous & not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 holds
f +* g is continuous
let f, g be PartFunc of REAL,REAL; :: thesis: ( g is continuous & not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 implies f +* g is continuous )
assume ( g is continuous & not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 ) ; :: 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 Kluczyk;
thus f +* g is continuous by A2; :: thesis: verum