let a, b be Real; 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; ( 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 )
; 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; verum