r in REAL by XREAL_0:def 1;
then reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:45;
assume that
A7: f . p < f . g and
A8: for s being Real st s in [.p,g.] holds
r <> f . s ; :: thesis: contradiction
[.(f . p),(f . g).] \/ [.(f . g),(f . p).] = [.(f . p),(f . g).] \/ {} by A7, XXREAL_1:29
.= [.(f . p),(f . g).] ;
then r in { s where s is Real : ( f . p <= s & s <= f . g ) } by A4, RCOMP_1:def 1;
then A9: ex s being Real st
( s = r & f . p <= s & s <= f . g ) ;
p in [.p,g.] by A1, XXREAL_1:1;
then A10: r <> f . p by A8;
reconsider f1 = f1 as PartFunc of REAL,REAL by RELSET_1:7;
A11: dom f1 = [.p,g.] by FUNCOP_1:13;
then A12: [.p,g.] c= (dom f1) /\ (dom f) by A2, XBOOLE_1:19;
then A13: [.p,g.] c= dom (f1 - f) by VALUED_1:12;
A14: (abs (f1 - f)) " {0} = {} A18: dom ((abs (f1 - f)) ^) = (dom (abs (f1 - f))) \ ((abs (f1 - f)) " {0}) by RFUNCT_1:def 2
.= dom (f1 - f) by A14, VALUED_1:def 11
.= [.p,g.] /\ (dom f) by A11, VALUED_1:12
.= [.p,g.] by A2, XBOOLE_1:28 ;
reconsider r = r as Element of REAL by XREAL_0:def 1;
for x0 being Element of REAL st x0 in [.p,g.] /\ (dom f1) holds
f1 . x0 = r by A11, FUNCOP_1:7;
then f1 | [.p,g.] is V8() by PARTFUN2:57;
then (f1 - f) | [.p,g.] is continuous by A3, A12, FCONT_1:18;
then (abs (f1 - f)) | [.p,g.] is continuous by A13, FCONT_1:21;
then ((abs (f1 - f)) ^) | [.p,g.] is continuous by A14, FCONT_1:22;
then ((abs (f1 - f)) ^) .: [.p,g.] is real-bounded by A5, A18, FCONT_1:29, RCOMP_1:10;
then consider M being Real such that
A19: M is UpperBound of ((abs (f1 - f)) ^) .: [.p,g.] by XXREAL_2:def 10;
A20: for x1 being Real st x1 in ((abs (f1 - f)) ^) .: [.p,g.] holds
x1 <= M by A19, XXREAL_2:def 1;
0 + 0 < |.M.| + 1 by COMPLEX1:46, XREAL_1:8;
then 0 < (|.M.| + 1) " ;
then A21: 0 < 1 / (|.M.| + 1) by XCMPLX_1:215;
f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:6;
then consider s being Real such that
A22: 0 < s and
A23: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < 1 / (|.M.| + 1) by A21, Th1;
hence contradiction ; :: thesis: verum

r in REAL by XREAL_0:def 1;
then reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:45;
assume that
A52: f . g < f . p and
A53: for s being Real st s in [.p,g.] holds
r <> f . s ; :: thesis: contradiction
[.(f . p),(f . g).] \/ [.(f . g),(f . p).] = {} \/ [.(f . g),(f . p).] by A52, XXREAL_1:29
.= [.(f . g),(f . p).] ;
then r in { s where s is Real : ( f . g <= s & s <= f . p ) } by A4, RCOMP_1:def 1;
then A54: ex s being Real st
( s = r & f . g <= s & s <= f . p ) ;
g in { s where s is Real : ( p <= s & s <= g ) } by A1;
then g in [.p,g.] by RCOMP_1:def 1;
then A55: r <> f . g by A53;
reconsider f1 = f1 as PartFunc of REAL,REAL by RELSET_1:7;
A56: dom f1 = [.p,g.] by FUNCOP_1:13;
then A57: [.p,g.] c= (dom f1) /\ (dom f) by A2, XBOOLE_1:19;
then A58: [.p,g.] c= dom (f1 - f) by VALUED_1:12;
A59: (abs (f1 - f)) " {0} = {} A63: dom ((abs (f1 - f)) ^) = (dom (abs (f1 - f))) \ ((abs (f1 - f)) " {0}) by RFUNCT_1:def 2
.= dom (f1 - f) by A59, VALUED_1:def 11
.= [.p,g.] /\ (dom f) by A56, VALUED_1:12
.= [.p,g.] by A2, XBOOLE_1:28 ;
reconsider r = r as Element of REAL by XREAL_0:def 1;
for x0 being Element of REAL st x0 in [.p,g.] /\ (dom f1) holds
f1 . x0 = r by A56, FUNCOP_1:7;
then f1 | [.p,g.] is V8() by PARTFUN2:57;
then (f1 - f) | [.p,g.] is continuous by A3, A57, FCONT_1:18;
then (abs (f1 - f)) | [.p,g.] is continuous by A58, FCONT_1:21;
then ((abs (f1 - f)) ^) | [.p,g.] is continuous by A59, FCONT_1:22;
then ((abs (f1 - f)) ^) .: [.p,g.] is real-bounded by A5, A63, FCONT_1:29, RCOMP_1:10;
then consider M being Real such that
A64: M is UpperBound of ((abs (f1 - f)) ^) .: [.p,g.] by XXREAL_2:def 10;
A65: for x1 being Real st x1 in ((abs (f1 - f)) ^) .: [.p,g.] holds
x1 <= M by A64, XXREAL_2:def 1;
0 + 0 < |.M.| + 1 by COMPLEX1:46, XREAL_1:8;
then 0 < (|.M.| + 1) " ;
then A66: 0 < 1 / (|.M.| + 1) by XCMPLX_1:215;
f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:6;
then consider s being Real such that
A67: 0 < s and
A68: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < 1 / (|.M.| + 1) by A66, Th1;
hence contradiction ; :: thesis: verum

assume A96: f . p = f . g ; :: thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
take p ; :: thesis: ( p in [.p,g.] & r = f . p )
thus p in [.p,g.] by A1, XXREAL_1:1; :: thesis: r = f . p
[.(f . p),(f . g).] \/ [.(f . g),(f . p).] = {(f . p)} by A96, XXREAL_1:17;
hence r = f . p by A4, TARSKI:def 1; :: thesis: verum