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_{1}( 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_{1}(x)
from FUNCT_2:sch 4();

A5: for x being Real holds h . x = min (b,(g . x))

for x being Real holds f . x = max (a,(h . x))

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

consider h being Function of REAL,REAL such that

A3: for x being Element of REAL holds h . x = H

A5: for x being Real holds h . x = min (b,(g . x))

proof

then A4:
h is continuous
by MMcon1, A1;
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;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

for x being Real holds f . x = max (a,(h . x))

proof

hence
f is continuous
by MMcon3, A4; :: thesis: verum
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;thus f . x = max (a,(min (b,(g . x)))) by A2

.= max (a,(h . x)) by A5 ; :: thesis: verum