let g, p be Real; :: thesis: for f being one-to-one PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds

(f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous

let f be one-to-one PartFunc of REAL,REAL; :: thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous )

assume that

A1: p <= g and

A2: [.p,g.] c= dom f and

A3: f | [.p,g.] is continuous ; :: thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous

(f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous

let f be one-to-one PartFunc of REAL,REAL; :: thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous )

assume that

A1: p <= g and

A2: [.p,g.] c= dom f and

A3: f | [.p,g.] is continuous ; :: thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous

now :: thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous end;

hence
(f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
; :: thesis: verumper cases
( f | [.p,g.] is increasing or f | [.p,g.] is decreasing )
by A1, A2, A3, Th17;

end;

suppose
f | [.p,g.] is increasing
; :: thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous

then
((f | [.p,g.]) ") | (f .: [.p,g.]) is increasing
by RFUNCT_2:51;

then ((f ") | (f .: [.p,g.])) | (f .: [.p,g.]) is increasing by RFUNCT_2:17;

then (f ") | (f .: [.p,g.]) is monotone by RELAT_1:72;

then A4: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is monotone by A1, A2, A3, Th19;

(f ") .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = (f ") .: (f .: [.p,g.]) by A1, A2, A3, Th19

.= ((f ") | (f .: [.p,g.])) .: (f .: [.p,g.]) by RELAT_1:129

.= ((f | [.p,g.]) ") .: (f .: [.p,g.]) by RFUNCT_2:17

.= ((f | [.p,g.]) ") .: (rng (f | [.p,g.])) by RELAT_1:115

.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33

.= rng ((f | [.p,g.]) ") by RELAT_1:113

.= dom (f | [.p,g.]) by FUNCT_1:33

.= (dom f) /\ [.p,g.] by RELAT_1:61

.= [.p,g.] by A2, XBOOLE_1:28 ;

hence (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous by A1, A4, FCONT_1:46; :: thesis: verum

end;then ((f ") | (f .: [.p,g.])) | (f .: [.p,g.]) is increasing by RFUNCT_2:17;

then (f ") | (f .: [.p,g.]) is monotone by RELAT_1:72;

then A4: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is monotone by A1, A2, A3, Th19;

(f ") .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = (f ") .: (f .: [.p,g.]) by A1, A2, A3, Th19

.= ((f ") | (f .: [.p,g.])) .: (f .: [.p,g.]) by RELAT_1:129

.= ((f | [.p,g.]) ") .: (f .: [.p,g.]) by RFUNCT_2:17

.= ((f | [.p,g.]) ") .: (rng (f | [.p,g.])) by RELAT_1:115

.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33

.= rng ((f | [.p,g.]) ") by RELAT_1:113

.= dom (f | [.p,g.]) by FUNCT_1:33

.= (dom f) /\ [.p,g.] by RELAT_1:61

.= [.p,g.] by A2, XBOOLE_1:28 ;

hence (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous by A1, A4, FCONT_1:46; :: thesis: verum

suppose
f | [.p,g.] is decreasing
; :: thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous

then
((f | [.p,g.]) ") | (f .: [.p,g.]) is decreasing
by RFUNCT_2:52;

then ((f ") | (f .: [.p,g.])) | (f .: [.p,g.]) is decreasing by RFUNCT_2:17;

then (f ") | (f .: [.p,g.]) is monotone by RELAT_1:72;

then A5: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is monotone by A1, A2, A3, Th19;

(f ") .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = (f ") .: (f .: [.p,g.]) by A1, A2, A3, Th19

.= ((f ") | (f .: [.p,g.])) .: (f .: [.p,g.]) by RELAT_1:129

.= ((f | [.p,g.]) ") .: (f .: [.p,g.]) by RFUNCT_2:17

.= ((f | [.p,g.]) ") .: (rng (f | [.p,g.])) by RELAT_1:115

.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33

.= rng ((f | [.p,g.]) ") by RELAT_1:113

.= dom (f | [.p,g.]) by FUNCT_1:33

.= (dom f) /\ [.p,g.] by RELAT_1:61

.= [.p,g.] by A2, XBOOLE_1:28 ;

hence (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous by A1, A5, FCONT_1:46; :: thesis: verum

end;then ((f ") | (f .: [.p,g.])) | (f .: [.p,g.]) is decreasing by RFUNCT_2:17;

then (f ") | (f .: [.p,g.]) is monotone by RELAT_1:72;

then A5: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is monotone by A1, A2, A3, Th19;

(f ") .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = (f ") .: (f .: [.p,g.]) by A1, A2, A3, Th19

.= ((f ") | (f .: [.p,g.])) .: (f .: [.p,g.]) by RELAT_1:129

.= ((f | [.p,g.]) ") .: (f .: [.p,g.]) by RFUNCT_2:17

.= ((f | [.p,g.]) ") .: (rng (f | [.p,g.])) by RELAT_1:115

.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33

.= rng ((f | [.p,g.]) ") by RELAT_1:113

.= dom (f | [.p,g.]) by FUNCT_1:33

.= (dom f) /\ [.p,g.] by RELAT_1:61

.= [.p,g.] by A2, XBOOLE_1:28 ;

hence (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous by A1, A5, FCONT_1:46; :: thesis: verum