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))

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

hence
f is continuous
by MMcon2, A3, A2; :: thesis: verum
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;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