let g, p be Real; 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; ( 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
; (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
now (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous per cases
( f | [.p,g.] is increasing or f | [.p,g.] is decreasing )
by A1, A2, A3, Th17;
suppose
f | [.p,g.] is
increasing
;
(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;
verum end; suppose
f | [.p,g.] is
decreasing
;
(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;
verum end; end; end;
hence
(f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
; verum