let f, g be Function of REAL,REAL; :: thesis: for a, b being Real st g is continuous & ( for x being Real holds f . x = max (a,(min (b,(g . x)))) ) holds
f is continuous
let a, b be Real; :: thesis: ( g is continuous & ( for x being Real holds f . x = max (a,(min (b,(g . x)))) ) implies f is continuous )
assume A1: g is continuous ; :: thesis: ( ex x being Real st not f . x = max (a,(min (b,(g . x)))) or f is continuous )
assume A2: for x being Real holds f . x = max (a,(min (b,(g . x)))) ; :: thesis: f is continuous
deffunc H₁( Element of REAL ) -> Element of REAL = In ((min (b,(g . $1))),REAL);
consider h being Function of REAL,REAL such that
A3: for x being Element of REAL holds h . x = H₁(x) from FUNCT_2:sch 4();
A5: for x being Real holds h . x = min (b,(g . x))

proof

let x be Real; :: thesis: h . x = min (b,(g . x))
reconsider x = x as Element of REAL by XREAL_0:def 1;
h . x = In ((min (b,(g . x))),REAL) by A3
.= min (b,(g . x)) ;
hence h . x = min (b,(g . x)) ; :: thesis: verum

end;

then A4: h is continuous by MMcon1, A1;
for x being Real holds f . x = max (a,(h . x))

proof

let x be Real; :: thesis: f . x = max (a,(h . x))
thus f . x = max (a,(min (b,(g . x)))) by A2
.= max (a,(h . x)) by A5 ; :: thesis: verum

end;

hence f is continuous by MMcon3, A4; :: thesis: verum