let p, g be Real; :: thesis:
assume A1: p < g ; :: thesis:
reconsider Z = ].p,g.[ as open Subset of REAL ;
let f be PartFunc of REAL,REAL; :: thesis:
assume that
A2: [.p,g.] c= dom f and
A3: f | [.p,g.] is continuous and
A4: f . p = f . g and
A5: f is_differentiable_on ].p,g.[ ; :: thesis:
A6: f .: [.p,g.] is compact by A2, A3, FCONT_1:29, RCOMP_1:6;
[.p,g.] is compact by RCOMP_1:6;
then A7: f .: [.p,g.] is real-bounded by A2, A3, FCONT_1:29, RCOMP_1:10;
p in [.p,g.] by A1, XXREAL_1:1;
then consider x1, x2 being Real such that
A8: x1 in [.p,g.] and
A9: x2 in [.p,g.] and
A10: f . x1 = upper_bound (f .: [.p,g.]) and
A11: f . x2 = lower_bound (f .: [.p,g.]) by A2, A3, FCONT_1:31, RCOMP_1:6;
reconsider x1 = x1, x2 = x2 as Element of REAL by XREAL_0:def 1;
p in { r where r is Real : ( p <= r & r <= g ) } by A1;
then p in [.p,g.] by RCOMP_1:def 1;
then f . p in f .: [.p,g.] by A2, FUNCT_1:def 6;
then A12: not f . x1 < f . x2 by A10, A11, A6, RCOMP_1:10, SEQ_4:11;
A13: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
then A14: ].p,g.[ c= dom f by A2;

per cases by A12, XXREAL_0:1;

suppose A15: f . x1 = f . x2 ; :: thesis:

p / 2 < g / 2 by A1, XREAL_1:74;
then ( (p / 2) + (g / 2) < (g / 2) + (g / 2) & (p / 2) + (p / 2) < (p / 2) + (g / 2) ) by XREAL_1:8;
then (p / 2) + (g / 2) in { r where r is Real : ( p < r & r < g ) } ;
then A16: (p / 2) + (g / 2) in Z by RCOMP_1:def 2;
f | [.p,g.] is V8() by A10, A11, A7, A15, RFUNCT_2:19;
then f | Z is V8() by PARTFUN2:38, XXREAL_1:25;
then (f `| Z) . ((p / 2) + (g / 2)) = 0 by A14, A16, FDIFF_1:22;
then diff (f,((p / 2) + (g / 2))) = 0 by A5, A16, FDIFF_1:def 7;
hence ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 ) by A16; :: thesis:

end;

suppose A17: f . x2 < f . x1 ; :: thesis:

A18: ( x2 in ].p,g.[ or x1 in ].p,g.[ )

proof

assume that
A19: not x2 in ].p,g.[ and
A20: not x1 in ].p,g.[ ; :: thesis:
x1 in ].p,g.[ \/ {p,g} by A1, A8, XXREAL_1:128;
then x1 in {p,g} by A20, XBOOLE_0:def 3;
then A21: ( x1 = p or x1 = g ) by TARSKI:def 2;
x2 in ].p,g.[ \/ {p,g} by A1, A9, XXREAL_1:128;
then x2 in {p,g} by A19, XBOOLE_0:def 3;
hence contradiction by A4, A17, A21, TARSKI:def 2; :: thesis:

end;

now :: thesis:

per cases by A18;

case A22: x2 in ].p,g.[ ; :: thesis:

then consider N1 being Neighbourhood of x2 such that
A23: N1 c= Z by RCOMP_1:18;
consider r being Real such that
A24: 0 < r and
A25: N1 = ].(x2 - r),(x2 + r).[ by RCOMP_1:def 6;
reconsider r = r as Real ;
deffunc H₁( Nat) -> set = r / ($1 + 2);
consider s2 being Real_Sequence such that
A26: for n being Nat holds s2 . n = H₁(n) from SEQ_1:sch 1();

now :: thesis:

let n be Nat; :: thesis:
0 <> r / (n + 2) by A24, XREAL_1:139;
hence 0 <> s2 . n by A26; :: thesis:

end;

then A27: s2 is non-zero by SEQ_1:5;
( s2 is convergent & lim s2 = 0 ) by A26, SEQ_4:31;
then reconsider h1 = s2 as non-zero 0 -convergent Real_Sequence by A27, FDIFF_1:def 1;
consider s1 being Real_Sequence such that
A28: rng s1 = {x2} by SEQ_1:6;
reconsider c = s1 as V8() Real_Sequence by A28, FUNCT_2:111;

A29: now :: thesis:

let n be Nat; :: thesis:
c . n in {x2} by A28, VALUED_0:28;
hence c . n = x2 by TARSKI:def 1; :: thesis:

end;

deffunc H₂( Nat) -> object = - (r / ($1 + 2));
consider s3 being Real_Sequence such that
A30: for n being Nat holds s3 . n = H₂(n) from SEQ_1:sch 1();

now :: thesis:

let n be Nat; :: thesis:
s3 . n = - (r / (n + 2)) by A30;
hence s3 . n = (- r) / (n + 2) ; :: thesis:

end;

then A31: ( s3 is convergent & lim s3 = 0 ) by SEQ_4:31;

now :: thesis:

let n be Nat; :: thesis:
- 0 <> - (r / (n + 2)) by A24, XREAL_1:139;
hence 0 <> s3 . n by A30; :: thesis:

end;

then s3 is non-zero by SEQ_1:5;
then reconsider h2 = s3 as non-zero 0 -convergent Real_Sequence by A31, FDIFF_1:def 1;
A32: N1 c= dom f by A14, A23;

A33: now :: thesis:

let n be Nat; :: thesis:
0 + 1 <= n + 1 by XREAL_1:6;
then 1 < (n + 1) + 1 by NAT_1:13;
then r / (n + 2) < r / 1 by A24, XREAL_1:76;
then A34: x2 - r < x2 - (r / (n + 2)) by XREAL_1:15;
x2 - (r / (n + 2)) < x2 + r by A24, XREAL_1:6;
then x2 - (r / (n + 2)) in { s where s is Real : ( x2 - r < s & s < x2 + r ) } by A34;
hence x2 - (r / (n + 2)) in N1 by A25, RCOMP_1:def 2; :: thesis:

end;

A35: rng (h2 + c) c= N1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (h2 + c) ; :: thesis:
then consider n being Element of NAT such that
A36: (h2 + c) . n = y by FUNCT_2:113;
y = (h2 . n) + (c . n) by A36, SEQ_1:7
.= (- (r / (n + 2))) + (c . n) by A30
.= x2 - (r / (n + 2)) by A29 ;
hence y in N1 by A33; :: thesis:

end;

A37: now :: thesis:

let n be Nat; :: thesis:
0 + 1 <= n + 1 by XREAL_1:6;
then 1 < (n + 1) + 1 by NAT_1:13;
then r / (n + 2) < r / 1 by A24, XREAL_1:76;
then A38: x2 + (r / (n + 2)) < x2 + r by XREAL_1:6;
0 < r / (n + 2) by A24, XREAL_1:139;
then x2 - r < x2 + (r / (n + 2)) by A24, XREAL_1:6;
then x2 + (r / (n + 2)) in { s where s is Real : ( x2 - r < s & s < x2 + r ) } by A38;
hence x2 + (r / (n + 2)) in N1 by A25, RCOMP_1:def 2; :: thesis:

end;

A39: rng (h1 + c) c= N1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (h1 + c) ; :: thesis:
then consider n being Element of NAT such that
A40: (h1 + c) . n = y by FUNCT_2:113;
y = (h1 . n) + (c . n) by A40, SEQ_1:7
.= (r / (n + 2)) + (c . n) by A26
.= x2 + (r / (n + 2)) by A29 ;
hence y in N1 by A37; :: thesis:

end;

A41: now :: thesis:

let n be Nat; :: thesis:
0 < r / (n + 2) by A24, XREAL_1:139;
hence 0 < s2 . n by A26; :: thesis:

end;

A42: for n being Nat holds 0 <= ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n

proof

let n be Nat; :: thesis:
A43: ( 0 < h1 . n & (h1 ") . n = (h1 . n) " ) by A41, VALUED_1:10;
(h1 + c) . n in rng (h1 + c) by VALUED_0:28;
then (h1 + c) . n in N1 by A39;
then (h1 + c) . n in Z by A23;
then f . ((h1 + c) . n) in f .: [.p,g.] by A13, A14, FUNCT_1:def 6;
then f . x2 <= f . ((h1 + c) . n) by A11, A7, SEQ_4:def 2;
then A44: 0 <= (f . ((h1 + c) . n)) - (f . x2) by XREAL_1:48;
reconsider n = n as Element of NAT by ORDINAL1:def 12;

now :: thesis:

let n1 be Element of NAT ; :: thesis:
(h1 + c) . n1 in rng (h1 + c) by VALUED_0:28;
then (h1 + c) . n1 in N1 by A39;
hence (h1 + c) . n1 in ].p,g.[ by A23; :: thesis:

end;

then A45: rng (h1 + c) c= ].p,g.[ by FUNCT_2:114;
A46: rng c c= dom f by A2, A9, A28, ZFMISC_1:31;
((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n = ((h1 ") . n) * (((f /* (h1 + c)) - (f /* c)) . n) by SEQ_1:8
.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - ((f /* c) . n)) by RFUNCT_2:1
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - ((f /* c) . n)) by A14, A45, FUNCT_2:108, XBOOLE_1:1
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - (f . (c . n))) by A46, FUNCT_2:108
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - (f . x2)) by A29 ;
hence 0 <= ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n by A44, A43; :: thesis:

end;

A47: f is_differentiable_in x2 by A5, A22, FDIFF_1:9;
then ( (h1 ") (#) ((f /* (h1 + c)) - (f /* c)) is convergent & diff (f,x2) = lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) ) by A32, A28, A39, FDIFF_1:12;
then A48: 0 <= diff (f,x2) by A42, SEQ_2:17;

A49: now :: thesis:

let n be Nat; :: thesis:
0 < r / (n + 2) by A24, XREAL_1:139;
then - (r / (n + 2)) < - 0 by XREAL_1:24;
hence s3 . n < 0 by A30; :: thesis:

end;

A50: for n being Nat holds ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n <= 0

proof

let n be Nat; :: thesis:

now :: thesis:

let n1 be Element of NAT ; :: thesis:
(h2 + c) . n1 in rng (h2 + c) by VALUED_0:28;
then (h2 + c) . n1 in N1 by A35;
hence (h2 + c) . n1 in ].p,g.[ by A23; :: thesis:

end;

then A51: rng (h2 + c) c= ].p,g.[ by FUNCT_2:114;
h2 . n < 0 by A49;
then - 0 < - (h2 . n) by XREAL_1:24;
then 0 < 1 / (- (h2 . n)) ;
then ( (h2 ") . n = (h2 . n) " & 0 < - (1 / (h2 . n)) ) by VALUED_1:10, XCMPLX_1:188;
then A52: (h2 ") . n <= 0 ;
(h2 + c) . n in rng (h2 + c) by VALUED_0:28;
then (h2 + c) . n in N1 by A35;
then (h2 + c) . n in Z by A23;
then f . ((h2 + c) . n) in f .: [.p,g.] by A13, A14, FUNCT_1:def 6;
then f . x2 <= f . ((h2 + c) . n) by A11, A7, SEQ_4:def 2;
then A53: 0 <= (f . ((h2 + c) . n)) - (f . x2) by XREAL_1:48;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A54: rng c c= dom f by A2, A9, A28, ZFMISC_1:31;
((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n = ((h2 ") . n) * (((f /* (h2 + c)) - (f /* c)) . n) by SEQ_1:8
.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - ((f /* c) . n)) by RFUNCT_2:1
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - ((f /* c) . n)) by A14, A51, FUNCT_2:108, XBOOLE_1:1
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - (f . (c . n))) by A54, FUNCT_2:108
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - (f . x2)) by A29 ;
hence ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n <= 0 by A53, A52; :: thesis:

end;

( (h2 ") (#) ((f /* (h2 + c)) - (f /* c)) is convergent & diff (f,x2) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) ) by A47, A32, A28, A35, FDIFF_1:12;
hence ( x2 in ].p,g.[ & diff (f,x2) = 0 ) by A22, A48, A50, RFUNCT_2:7; :: thesis:

end;

case A55: x1 in ].p,g.[ ; :: thesis:

then consider N1 being Neighbourhood of x1 such that
A56: N1 c= ].p,g.[ by RCOMP_1:18;
consider r being Real such that
A57: 0 < r and
A58: N1 = ].(x1 - r),(x1 + r).[ by RCOMP_1:def 6;
reconsider r = r as Real ;
deffunc H₁( Nat) -> set = r / ($1 + 2);
consider s2 being Real_Sequence such that
A59: for n being Nat holds s2 . n = H₁(n) from SEQ_1:sch 1();

now :: thesis:

let n be Nat; :: thesis:
0 <> r / (n + 2) by A57, XREAL_1:139;
hence 0 <> s2 . n by A59; :: thesis:

end;

then A60: s2 is non-zero by SEQ_1:5;
( s2 is convergent & lim s2 = 0 ) by A59, SEQ_4:31;
then reconsider h1 = s2 as non-zero 0 -convergent Real_Sequence by A60, FDIFF_1:def 1;
consider s1 being Real_Sequence such that
A61: rng s1 = {x1} by SEQ_1:6;
reconsider c = s1 as V8() Real_Sequence by A61, FUNCT_2:111;

A62: now :: thesis:

let n be Nat; :: thesis:
c . n in {x1} by A61, VALUED_0:28;
hence c . n = x1 by TARSKI:def 1; :: thesis:

end;

deffunc H₂( Nat) -> object = - (r / ($1 + 2));
consider s3 being Real_Sequence such that
A63: for n being Nat holds s3 . n = H₂(n) from SEQ_1:sch 1();

now :: thesis:

let n be Nat; :: thesis:
s3 . n = - (r / (n + 2)) by A63;
hence s3 . n = (- r) / (n + 2) ; :: thesis:

end;

then A64: ( s3 is convergent & lim s3 = 0 ) by SEQ_4:31;

now :: thesis:

let n be Nat; :: thesis:
- 0 <> - (r / (n + 2)) by A57, XREAL_1:139;
hence 0 <> s3 . n by A63; :: thesis:

end;

then s3 is non-zero by SEQ_1:5;
then reconsider h2 = s3 as non-zero 0 -convergent Real_Sequence by A64, FDIFF_1:def 1;
A65: N1 c= dom f by A14, A56;

A66: now :: thesis:

let n be Nat; :: thesis:
0 + 1 <= n + 1 by XREAL_1:6;
then 1 < (n + 1) + 1 by NAT_1:13;
then r / (n + 2) < r / 1 by A57, XREAL_1:76;
then A67: x1 - r < x1 - (r / (n + 2)) by XREAL_1:15;
x1 - (r / (n + 2)) < x1 + r by A57, XREAL_1:6;
then x1 - (r / (n + 2)) in { s where s is Real : ( x1 - r < s & s < x1 + r ) } by A67;
hence x1 - (r / (n + 2)) in N1 by A58, RCOMP_1:def 2; :: thesis:

end;

A68: rng (h2 + c) c= N1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (h2 + c) ; :: thesis:
then consider n being Element of NAT such that
A69: (h2 + c) . n = y by FUNCT_2:113;
y = (h2 . n) + (c . n) by A69, SEQ_1:7
.= (- (r / (n + 2))) + (c . n) by A63
.= x1 - (r / (n + 2)) by A62 ;
hence y in N1 by A66; :: thesis:

end;

A70: now :: thesis:

let n be Nat; :: thesis:
0 + 1 <= n + 1 by XREAL_1:6;
then 1 < (n + 1) + 1 by NAT_1:13;
then r / (n + 2) < r / 1 by A57, XREAL_1:76;
then A71: x1 + (r / (n + 2)) < x1 + r by XREAL_1:6;
0 < r / (n + 2) by A57, XREAL_1:139;
then x1 - r < x1 + (r / (n + 2)) by A57, XREAL_1:6;
then x1 + (r / (n + 2)) in { s where s is Real : ( x1 - r < s & s < x1 + r ) } by A71;
hence x1 + (r / (n + 2)) in N1 by A58, RCOMP_1:def 2; :: thesis:

end;

A72: rng (h1 + c) c= N1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (h1 + c) ; :: thesis:
then consider n being Element of NAT such that
A73: (h1 + c) . n = y by FUNCT_2:113;
y = (h1 . n) + (c . n) by A73, SEQ_1:7
.= (r / (n + 2)) + (c . n) by A59
.= x1 + (r / (n + 2)) by A62 ;
hence y in N1 by A70; :: thesis:

end;

A74: now :: thesis:

let n be Nat; :: thesis:
0 < r / (n + 2) by A57, XREAL_1:139;
hence 0 < s2 . n by A59; :: thesis:

end;

A75: for n being Nat holds ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n <= 0

proof

let n be Nat; :: thesis:
A76: ( 0 < h1 . n & (h1 ") . n = (h1 . n) " ) by A74, VALUED_1:10;
(h1 + c) . n in rng (h1 + c) by VALUED_0:28;
then (h1 + c) . n in N1 by A72;
then (h1 + c) . n in Z by A56;
then f . ((h1 + c) . n) in f .: [.p,g.] by A13, A14, FUNCT_1:def 6;
then f . ((h1 + c) . n) <= f . x1 by A10, A7, SEQ_4:def 1;
then 0 <= (f . x1) - (f . ((h1 + c) . n)) by XREAL_1:48;
then A77: - ((f . x1) - (f . ((h1 + c) . n))) <= - 0 ;

now :: thesis:

let n1 be Element of NAT ; :: thesis:
(h1 + c) . n1 in rng (h1 + c) by VALUED_0:28;
then (h1 + c) . n1 in N1 by A72;
hence (h1 + c) . n1 in ].p,g.[ by A56; :: thesis:

end;

then A78: rng (h1 + c) c= ].p,g.[ by FUNCT_2:114;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A79: rng c c= dom f by A2, A8, A61, ZFMISC_1:31;
((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n = ((h1 ") . n) * (((f /* (h1 + c)) - (f /* c)) . n) by SEQ_1:8
.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - ((f /* c) . n)) by RFUNCT_2:1
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - ((f /* c) . n)) by A14, A78, FUNCT_2:108, XBOOLE_1:1
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - (f . (c . n))) by A79, FUNCT_2:108
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - (f . x1)) by A62 ;
hence ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n <= 0 by A77, A76; :: thesis:

end;

A80: f is_differentiable_in x1 by A5, A55, FDIFF_1:9;
then ( (h1 ") (#) ((f /* (h1 + c)) - (f /* c)) is convergent & diff (f,x1) = lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) ) by A65, A61, A72, FDIFF_1:12;
then A81: diff (f,x1) <= 0 by A75, RFUNCT_2:7;

A82: now :: thesis:

let n be Nat; :: thesis:
0 < r / (n + 2) by A57, XREAL_1:139;
then - (r / (n + 2)) < - 0 by XREAL_1:24;
hence s3 . n < 0 by A63; :: thesis:

end;

A83: for n being Nat holds 0 <= ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n

proof

let n be Nat; :: thesis:

now :: thesis:

let n1 be Element of NAT ; :: thesis:
(h2 + c) . n1 in rng (h2 + c) by VALUED_0:28;
then (h2 + c) . n1 in N1 by A68;
hence (h2 + c) . n1 in ].p,g.[ by A56; :: thesis:

end;

then A84: rng (h2 + c) c= ].p,g.[ by FUNCT_2:114;
h2 . n < 0 by A82;
then - 0 < - (h2 . n) by XREAL_1:24;
then 0 < 1 / (- (h2 . n)) ;
then ( (h2 ") . n = (h2 . n) " & 0 < - (1 / (h2 . n)) ) by VALUED_1:10, XCMPLX_1:188;
then A85: (h2 ") . n <= 0 ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
(h2 + c) . n in rng (h2 + c) by VALUED_0:28;
then (h2 + c) . n in N1 by A68;
then (h2 + c) . n in Z by A56;
then f . ((h2 + c) . n) in f .: [.p,g.] by A13, A14, FUNCT_1:def 6;
then f . ((h2 + c) . n) <= f . x1 by A10, A7, SEQ_4:def 1;
then 0 <= (f . x1) - (f . ((h2 + c) . n)) by XREAL_1:48;
then A86: - ((f . x1) - (f . ((h2 + c) . n))) <= - 0 ;
A87: rng c c= dom f by A2, A8, A61, ZFMISC_1:31;
((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n = ((h2 ") . n) * (((f /* (h2 + c)) - (f /* c)) . n) by SEQ_1:8
.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - ((f /* c) . n)) by RFUNCT_2:1
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - ((f /* c) . n)) by A14, A84, FUNCT_2:108, XBOOLE_1:1
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - (f . (c . n))) by A87, FUNCT_2:108
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - (f . x1)) by A62 ;
hence 0 <= ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n by A86, A85; :: thesis:

end;

( (h2 ") (#) ((f /* (h2 + c)) - (f /* c)) is convergent & diff (f,x1) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) ) by A80, A65, A61, A68, FDIFF_1:12;
hence ( x1 in ].p,g.[ & diff (f,x1) = 0 ) by A55, A81, A83, SEQ_2:17; :: thesis:

end;

hence ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 ) ; :: thesis:

end;