let f, g be Function of REAL,REAL; :: thesis: for a being Real st g is continuous & ( for x being Real holds f . x = max (a,(g . x)) ) holds
f is continuous
let a be Real; :: thesis: ( g is continuous & ( for x being Real holds f . x = max (a,(g . x)) ) implies f is continuous )
assume A3: g is continuous ; :: thesis: ( ex x being Real st not f . x = max (a,(g . x)) or f is continuous )
assume A0: for x being Real holds f . x = max (a,(g . x)) ; :: thesis: f is continuous
consider h being Function of REAL,REAL such that
A2: h = AffineMap (0,a) ;
for x being Real holds f . x = max ((h . x),(g . x))
proof
let x be Real; :: thesis: f . x = max ((h . x),(g . x))
f . x = max (((0 * x) + a),(g . x)) by A0
.= max (((AffineMap (0,a)) . x),(g . x)) by FCONT_1:def 4 ;
hence f . x = max ((h . x),(g . x)) by A2; :: thesis: verum
end;
hence f is continuous by MMcon2, A3, A2; :: thesis: verum