let g, p be Real; :: thesis: for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
let f be PartFunc of REAL,REAL; :: thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] & r = f . s ) )
assume that
A1: p <= g and
A2: [.p,g.] c= dom f and
A3: f | [.p,g.] is continuous ; :: thesis: for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
let r be Real; :: thesis: ( r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
assume A4: r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] ; :: thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
A5: [.p,g.] is compact by RCOMP_1:6;
A6: ( f . p < f . g implies ex s being Real st
( s in [.p,g.] & r = f . s ) )

proof

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} = {}

proof

assume (abs (f1 - f)) " {0} <> {} ; :: thesis: contradiction
then consider x2 being Element of REAL such that
A15: x2 in (abs (f1 - f)) " {0} by SUBSET_1:4;
x2 in dom (abs (f1 - f)) by A15, FUNCT_1:def 7;
then A16: x2 in dom (f1 - f) by VALUED_1:def 11;
then x2 in (dom f1) /\ (dom f) by VALUED_1:12;
then A17: x2 in [.p,g.] by A11, XBOOLE_0:def 4;
(abs (f1 - f)) . x2 in {0} by A15, FUNCT_1:def 7;
then (abs (f1 - f)) . x2 = 0 by TARSKI:def 1;
then |.((f1 - f) . x2).| = 0 by VALUED_1:18;
then (f1 - f) . x2 = 0 by ABSVALUE:2;
then (f1 . x2) - (f . x2) = 0 by A16, VALUED_1:13;
then r - (f . x2) = 0 by A17, FUNCOP_1:7;
hence contradiction by A8, A17; :: thesis: verum

end;

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 constant 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;

A24: now :: thesis: for x1 being Real st x1 in [.p,g.] holds
1 / (|.M.| + 1) < |.(r - (f . x1)).|

let x1 be Real; :: thesis: ( x1 in [.p,g.] implies 1 / (|.M.| + 1) < |.(r - (f . x1)).| )
assume A25: x1 in [.p,g.] ; :: thesis: 1 / (|.M.| + 1) < |.(r - (f . x1)).|
then ((abs (f1 - f)) ^) . x1 in ((abs (f1 - f)) ^) .: [.p,g.] by A18, FUNCT_1:def 6;
then ((abs (f1 - f)) ^) . x1 <= M by A20;
then ((abs (f1 - f)) . x1) " <= M by A18, A25, RFUNCT_1:def 2;
then A26: |.((f1 - f) . x1).| " <= M by VALUED_1:18;
x1 in (dom f1) /\ (dom f) by A2, A11, A25, XBOOLE_0:def 4;
then x1 in dom (f1 - f) by VALUED_1:12;
then |.((f1 . x1) - (f . x1)).| " <= M by A26, VALUED_1:13;
then A27: |.(r - (f . x1)).| " <= M by A25, FUNCOP_1:7;
r - (f . x1) <> 0 by A8, A25;
then A28: 0 < |.(r - (f . x1)).| by COMPLEX1:47;
M + 0 < |.M.| + 1 by ABSVALUE:4, XREAL_1:8;
then |.(r - (f . x1)).| " < |.M.| + 1 by A27, XXREAL_0:2;
then 1 / (|.M.| + 1) < 1 / (|.(r - (f . x1)).| ") by A28, XREAL_1:76;
hence 1 / (|.M.| + 1) < |.(r - (f . x1)).| by XCMPLX_1:216; :: thesis: verum

end;

now :: thesis: contradiction

per cases ( p = g or p <> g ) ;

suppose p = g ; :: thesis: contradiction

hence contradiction by A7; :: thesis: verum

end;

suppose p <> g ; :: thesis: contradiction

then p < g by A1, XXREAL_0:1;
then A29: 0 < g - p by XREAL_1:50;
then A30: 0 < (g - p) / s by A22, XREAL_1:139;
consider k being Nat such that
A31: (g - p) / s < k by SEQ_4:3;
((g - p) / s) * s < s * k by A22, A31, XREAL_1:68;
then g - p < s * k by A22, XCMPLX_1:87;
then (g - p) / k < (s * k) / k by A31, A30, XREAL_1:74;
then (g - p) / k < (s * k) * (k ") by XCMPLX_0:def 9;
then (g - p) / k < s * (k * (k ")) ;
then A32: (g - p) / k < s * 1 by A31, A30, XCMPLX_0:def 7;
deffunc H₁( Nat) -> set = p + (((g - p) / k) * $1);
consider s1 being Real_Sequence such that
A33: for n being Nat holds s1 . n = H₁(n) from SEQ_1:sch 1();
A34: 0 < (g - p) / k by A29, A31, A30, XREAL_1:139;

A35: now :: thesis: for n being Element of NAT st n < k holds
( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

let n be Element of NAT ; :: thesis: ( n < k implies ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) ) )
A36: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:62;
assume A37: n < k ; :: thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )
then ((g - p) / k) * n < ((g - p) / k) * k by A34, XREAL_1:68;
then ((g - p) / k) * n < g - p by A31, A30, XCMPLX_1:87;
then p + (((g - p) / k) * n) < p + (g - p) by XREAL_1:6;
then A38: s1 . n < p + (g - p) by A33;
n + 1 <= k by A37, NAT_1:13;
then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A29, XREAL_1:64;
then ((g - p) / k) * (n + 1) <= g - p by A31, A30, XCMPLX_1:87;
then p + (((g - p) / k) * (n + 1)) <= p + (g - p) by XREAL_1:7;
then A39: s1 . (n + 1) <= p + (g - p) by A33;
p + 0 <= p + (((g - p) / k) * n) by A29, XREAL_1:7;
then p <= s1 . n by A33;
then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A38;
hence A40: s1 . n in [.p,g.] by RCOMP_1:def 1; :: thesis: ( s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )
p + 0 <= p + (((g - p) / k) * (n + 1)) by A29, XREAL_1:7;
then p <= s1 . (n + 1) by A33;
then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A39;
hence A41: s1 . (n + 1) in [.p,g.] by RCOMP_1:def 1; :: thesis: |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1)
|.((s1 . (n + 1)) - (s1 . n)).| = |.((p + (((g - p) / k) * (n + 1))) - (s1 . n)).| by A33
.= |.((p + (((g - p) / k) * (n + 1))) - (p + (((g - p) / k) * n))).| by A33
.= (g - p) / k by A29, ABSVALUE:def 1 ;
hence |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) by A23, A32, A40, A41, A36; :: thesis: verum

end;

defpred S₁[ Nat] means r <= f . (s1 . $1);
A42: s1 . k = p + (((g - p) / k) * k) by A33
.= p + (g - p) by A31, A30, XCMPLX_1:87
.= g ;
then A43: ex n being Nat st S₁[n] by A9;
consider l being Nat such that
A44: ( S₁[l] & ( for m being Nat st S₁[m] holds
l <= m ) ) from NAT_1:sch 5(A43);
s1 . 0 = p + (((g - p) / k) * 0) by A33
.= p ;
then l <> 0 by A9, A10, A44, XXREAL_0:1;
then consider l1 being Nat such that
A45: l = l1 + 1 by NAT_1:6;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def 12;
A46: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A44, A45, XREAL_1:9;
l1 + 1 <= k by A9, A42, A44, A45;
then A47: l1 < k by NAT_1:13;
then A48: |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| < 1 / (|.M.| + 1) by A35;
f . (s1 . l1) < r

proof

assume r <= f . (s1 . l1) ; :: thesis: contradiction
then l <= l1 by A44;
then l + 0 < l by A45, XREAL_1:8;
hence contradiction ; :: thesis: verum

end;

then A49: 0 < r - (f . (s1 . l1)) by XREAL_1:50;
then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A44, A45, XREAL_1:9;
then |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def 1;
then A50: |.(r - (f . (s1 . l1))).| <= |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| by A49, A46, ABSVALUE:def 1;
s1 . l1 in [.p,g.] by A35, A47;
hence contradiction by A24, A50, A48, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A51: ( f . g < f . p implies ex s being Real st
( s in [.p,g.] & r = f . s ) )

proof

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} = {}

proof

assume (abs (f1 - f)) " {0} <> {} ; :: thesis: contradiction
then consider x2 being Element of REAL such that
A60: x2 in (abs (f1 - f)) " {0} by SUBSET_1:4;
x2 in dom (abs (f1 - f)) by A60, FUNCT_1:def 7;
then A61: x2 in dom (f1 - f) by VALUED_1:def 11;
then x2 in (dom f1) /\ (dom f) by VALUED_1:12;
then A62: x2 in [.p,g.] by A56, XBOOLE_0:def 4;
(abs (f1 - f)) . x2 in {0} by A60, FUNCT_1:def 7;
then (abs (f1 - f)) . x2 = 0 by TARSKI:def 1;
then |.((f1 - f) . x2).| = 0 by VALUED_1:18;
then (f1 - f) . x2 = 0 by ABSVALUE:2;
then (f1 . x2) - (f . x2) = 0 by A61, VALUED_1:13;
then r - (f . x2) = 0 by A62, FUNCOP_1:7;
hence contradiction by A53, A62; :: thesis: verum

end;

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 constant 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;

A69: now :: thesis: for x1 being Real st x1 in [.p,g.] holds
1 / (|.M.| + 1) < |.(r - (f . x1)).|

let x1 be Real; :: thesis: ( x1 in [.p,g.] implies 1 / (|.M.| + 1) < |.(r - (f . x1)).| )
assume A70: x1 in [.p,g.] ; :: thesis: 1 / (|.M.| + 1) < |.(r - (f . x1)).|
then ((abs (f1 - f)) ^) . x1 in ((abs (f1 - f)) ^) .: [.p,g.] by A63, FUNCT_1:def 6;
then ((abs (f1 - f)) ^) . x1 <= M by A65;
then ((abs (f1 - f)) . x1) " <= M by A63, A70, RFUNCT_1:def 2;
then A71: |.((f1 - f) . x1).| " <= M by VALUED_1:18;
x1 in (dom f1) /\ (dom f) by A2, A56, A70, XBOOLE_0:def 4;
then x1 in dom (f1 - f) by VALUED_1:12;
then |.((f1 . x1) - (f . x1)).| " <= M by A71, VALUED_1:13;
then A72: |.(r - (f . x1)).| " <= M by A70, FUNCOP_1:7;
r - (f . x1) <> 0 by A53, A70;
then A73: 0 < |.(r - (f . x1)).| by COMPLEX1:47;
M + 0 < |.M.| + 1 by ABSVALUE:4, XREAL_1:8;
then |.(r - (f . x1)).| " < |.M.| + 1 by A72, XXREAL_0:2;
then 1 / (|.M.| + 1) < 1 / (|.(r - (f . x1)).| ") by A73, XREAL_1:76;
hence 1 / (|.M.| + 1) < |.(r - (f . x1)).| by XCMPLX_1:216; :: thesis: verum

end;

now :: thesis: contradiction

per cases ( p = g or p <> g ) ;

suppose p = g ; :: thesis: contradiction

hence contradiction by A52; :: thesis: verum

end;

suppose p <> g ; :: thesis: contradiction

then p < g by A1, XXREAL_0:1;
then A74: 0 < g - p by XREAL_1:50;
then A75: 0 < (g - p) / s by A67, XREAL_1:139;
consider k being Nat such that
A76: (g - p) / s < k by SEQ_4:3;
((g - p) / s) * s < s * k by A67, A76, XREAL_1:68;
then g - p < s * k by A67, XCMPLX_1:87;
then (g - p) / k < (s * k) / k by A76, A75, XREAL_1:74;
then (g - p) / k < (s * k) * (k ") by XCMPLX_0:def 9;
then (g - p) / k < s * (k * (k ")) ;
then A77: (g - p) / k < s * 1 by A76, A75, XCMPLX_0:def 7;
deffunc H₁( Nat) -> set = g - (((g - p) / k) * $1);
consider s1 being Real_Sequence such that
A78: for n being Nat holds s1 . n = H₁(n) from SEQ_1:sch 1();
A79: 0 < (g - p) / k by A74, A76, A75, XREAL_1:139;

A80: now :: thesis: for n being Element of NAT st n < k holds
( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

let n be Element of NAT ; :: thesis: ( n < k implies ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) ) )
A81: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:62;
assume A82: n < k ; :: thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )
then ((g - p) / k) * n < ((g - p) / k) * k by A79, XREAL_1:68;
then ((g - p) / k) * n < g - p by A76, A75, XCMPLX_1:87;
then g - (g - p) < g - (((g - p) / k) * n) by XREAL_1:15;
then A83: g - (g - p) < s1 . n by A78;
n + 1 <= k by A82, NAT_1:13;
then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A74, XREAL_1:64;
then ((g - p) / k) * (n + 1) <= g - p by A76, A75, XCMPLX_1:87;
then g - (g - p) <= g - (((g - p) / k) * (n + 1)) by XREAL_1:13;
then A84: g - (g - p) <= s1 . (n + 1) by A78;
g - (((g - p) / k) * n) <= g - 0 by A74, XREAL_1:13;
then s1 . n <= g by A78;
then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A83;
hence A85: s1 . n in [.p,g.] by RCOMP_1:def 1; :: thesis: ( s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )
g - (((g - p) / k) * (n + 1)) <= g - 0 by A74, XREAL_1:13;
then s1 . (n + 1) <= g by A78;
then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A84;
hence A86: s1 . (n + 1) in [.p,g.] by RCOMP_1:def 1; :: thesis: |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1)
|.((s1 . (n + 1)) - (s1 . n)).| = |.((g - (((g - p) / k) * (n + 1))) - (s1 . n)).| by A78
.= |.((g - (((g - p) / k) * (n + 1))) - (g - (((g - p) / k) * n))).| by A78
.= |.(- ((((g - p) / k) * (n + 1)) - (((g - p) / k) * n))).|
.= |.(((g - p) / k) * ((n + 1) - n)).| by COMPLEX1:52
.= (g - p) / k by A74, ABSVALUE:def 1 ;
hence |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) by A68, A77, A85, A86, A81; :: thesis: verum

end;

defpred S₁[ Nat] means r <= f . (s1 . $1);
A87: s1 . k = g - (((g - p) / k) * k) by A78
.= g - (g - p) by A76, A75, XCMPLX_1:87
.= p ;
then A88: ex n being Nat st S₁[n] by A54;
consider l being Nat such that
A89: ( S₁[l] & ( for m being Nat st S₁[m] holds
l <= m ) ) from NAT_1:sch 5(A88);
s1 . 0 = g - (((g - p) / k) * 0) by A78
.= g ;
then l <> 0 by A54, A55, A89, XXREAL_0:1;
then consider l1 being Nat such that
A90: l = l1 + 1 by NAT_1:6;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def 12;
A91: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A89, A90, XREAL_1:9;
l1 + 1 <= k by A54, A87, A89, A90;
then A92: l1 < k by NAT_1:13;
then A93: |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| < 1 / (|.M.| + 1) by A80;
f . (s1 . l1) < r

proof

assume r <= f . (s1 . l1) ; :: thesis: contradiction
then l <= l1 by A89;
then l + 0 < l by A90, XREAL_1:8;
hence contradiction ; :: thesis: verum

end;

then A94: 0 < r - (f . (s1 . l1)) by XREAL_1:50;
then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A89, A90, XREAL_1:9;
then |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def 1;
then A95: |.(r - (f . (s1 . l1))).| <= |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| by A94, A91, ABSVALUE:def 1;
s1 . l1 in [.p,g.] by A80, A92;
hence contradiction by A69, A95, A93, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

( f . p = f . g implies ex s being Real st
( s in [.p,g.] & r = f . s ) )

proof

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

end;

hence ex s being Real st
( s in [.p,g.] & r = f . s ) by A6, A51, XXREAL_0:1; :: thesis: verum