:: Average Value Theorems for Real Functions of One Variable
::  by Jaros{\l}aw Kotowicz, Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, ARYTM_3, XXREAL_1,
      TARSKI, RELAT_1, ORDINAL2, FUNCT_1, FDIFF_1, CARD_1, RCOMP_1, XXREAL_2,
      XREAL_0, ORDINAL1, SEQ_4, XXREAL_0, XBOOLE_0, ARYTM_1, VALUED_0, SEQ_2,
      VALUED_1, FUNCT_2, FUNCOP_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0,
      XXREAL_0, XXREAL_2, REAL_1, RELSET_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2,
      SEQ_4, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1, FDIFF_1;
 constructors PARTFUN1, REAL_1, NAT_1, SEQ_2, SEQ_4, RCOMP_1, PARTFUN2,
      RFUNCT_2, FCONT_1, FDIFF_1, VALUED_1, SEQ_1, XXREAL_2, COMPLEX1,
      RELSET_1, BINOP_2, COMSEQ_2;
 registrations XBOOLE_0, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED,
      RCOMP_1, FDIFF_1, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, FCONT_1,
      ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, RFUNCT_2, XCMPLX_0;
 theorems TARSKI, NAT_1, SEQ_1, SEQ_2, SEQ_4, PARTFUN2, RFUNCT_2, RCOMP_1,
      FCONT_1, FDIFF_1, ZFMISC_1, FUNCT_1, XREAL_0, XBOOLE_0, XBOOLE_1,
      XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, XXREAL_2, XXREAL_1,
      FUNCT_2, VALUED_0;
 schemes SEQ_1;

begin

reserve y for set;
reserve g,r,s,p,t,x,x0,x1,x2 for Real;
reserve n,n1 for Element of NAT;
reserve s1,s2,s3 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL,REAL;

theorem Th1:
  for p,g st p<g for f st [.p,g.] c= dom f & f|[.p,g.] is
continuous & f.p=f.g & f is_differentiable_on ].p,g.[ ex x0 st x0 in ].p,g.[ &
  diff(f,x0)=0
proof
  let p,g such that
A1: p<g;
  reconsider Z=].p,g.[ as open Subset of REAL;
  let f such 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.[;
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 be real number 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,x2 as Real by XREAL_0:def 1;
  p in {r: 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,XBOOLE_1:1;
  per cases by A12,XXREAL_0:1;
  suppose
A15: f.x1 = f.x2;
    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: p<r & r<g};
    then
A16: p/2+g/2 in Z by RCOMP_1:def 2;
    f|[.p,g.] is constant by A10,A11,A7,A15,RFUNCT_2:19;
    then f|Z is constant 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 thesis by A16;
  end;
  suppose
A17: f.x2 < f.x1;
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.[;
      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;
    end;
    now
      per cases by A18;
      case
A22:    x2 in ].p,g.[;
        then consider N1 be Neighbourhood of x2 such that
A23:    N1 c= Z by RCOMP_1:18;
        consider r be real number such that
A24:    0<r and
A25:    N1=].x2-r,x2+r.[ by RCOMP_1:def 6;
        reconsider r as Real by XREAL_0:def 1;
        deffunc F(Element of NAT)=r/($1+2);
        consider s2 such that
A26:    for n holds s2.n=F(n) from SEQ_1:sch 1;
        now
          let n;
          0<>r/(n+2) by A24,XREAL_1:139;
          hence 0<>s2.n by A26;
        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 0-convergent non-zero Real_Sequence by A27,
FDIFF_1:def 1;
        consider s1 such that
A28:    rng s1 = {x2} by SEQ_1:6;
        reconsider c = s1 as constant Real_Sequence by A28,FUNCT_2:111;
A29:    now
          let n;
          c.n in {x2} by A28,VALUED_0:28;
          hence c.n = x2 by TARSKI:def 1;
        end;
        deffunc G(Element of NAT) = -(r/($1+2));
        consider s3 such that
A30:    for n holds s3.n=G(n) from SEQ_1:sch 1;
        now
          let n;
          s3.n = -(r/(n+2)) by A30;
          hence s3.n = (-r)/(n+2);
        end;
        then
A31:    s3 is convergent & lim s3 = 0 by SEQ_4:31;
        now
          let n;
          -0<>-(r/(n+2)) by A24,XREAL_1:139;
          hence 0<>s3.n by A30;
        end;
        then s3 is non-zero by SEQ_1:5;
        then reconsider h2 = s3 as 0-convergent non-zero Real_Sequence by A31,
FDIFF_1:def 1;
A32:    N1 c= dom f by A14,A23,XBOOLE_1:1;
A33:    now
          let n;
          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: x2-r<s & s<x2+r} by A34;
          hence x2-r/(n+2) in N1 by A25,RCOMP_1:def 2;
        end;
A35:    rng (h2+c) c= N1
        proof
          let y;
          assume y in rng (h2+c);
          then consider n 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 thesis by A33;
        end;
A37:    now
          let n;
          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: x2-r<s & s<x2+r} by A38;
          hence x2+r/(n+2) in N1 by A25,RCOMP_1:def 2;
        end;
A39:    rng (h1+c) c= N1
        proof
          let y;
          assume y in rng (h1+c);
          then consider n 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 thesis by A37;
        end;
A41:    now
          let n;
          0<r/(n+2) by A24,XREAL_1:139;
          hence 0<s2.n by A26;
        end;
A42:    for n holds 0<=(h1"(#)(f/*(h1+c) - f/*c)).n
        proof
          let n;
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;
          now
            let n1;
            (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;
          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 thesis by A44,A43;
        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
          let n;
          0<r/(n+2) by A24,XREAL_1:139;
          then -(r/(n+2))<-0 by XREAL_1:24;
          hence s3.n<0 by A30;
        end;
A50:    for n holds (h2"(#)(f/*(h2+c) - f/*c)).n <= 0
        proof
          let n;
          now
            let n1;
            (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;
          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;
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 thesis by A53,A52;
        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;
      end;
      case
A55:    x1 in ].p,g.[;
        then consider N1 be Neighbourhood of x1 such that
A56:    N1 c= ].p,g.[ by RCOMP_1:18;
        consider r be real number such that
A57:    0<r and
A58:    N1=].x1-r,x1+r.[ by RCOMP_1:def 6;
        reconsider r as Real by XREAL_0:def 1;
        deffunc F(Element of NAT) = r/($1+2);
        consider s2 such that
A59:    for n holds s2.n=F(n) from SEQ_1:sch 1;
        now
          let n;
          0<>r/(n+2) by A57,XREAL_1:139;
          hence 0<>s2.n by A59;
        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 0-convergent non-zero Real_Sequence by A60,
FDIFF_1:def 1;
        consider s1 such that
A61:    rng s1 = {x1} by SEQ_1:6;
        reconsider c = s1 as constant Real_Sequence by A61,FUNCT_2:111;
A62:    now
          let n;
          c.n in {x1} by A61,VALUED_0:28;
          hence c.n = x1 by TARSKI:def 1;
        end;
        deffunc G(Element of NAT) = -(r/($1+2));
        consider s3 such that
A63:    for n holds s3.n=G(n) from SEQ_1:sch 1;
        now
          let n;
          s3.n = -(r/(n+2)) by A63;
          hence s3.n = (-r)/(n+2);
        end;
        then
A64:    s3 is convergent & lim s3 = 0 by SEQ_4:31;
        now
          let n;
          -0<>-(r/(n+2)) by A57,XREAL_1:139;
          hence 0<>s3.n by A63;
        end;
        then s3 is non-zero by SEQ_1:5;
        then reconsider h2 = s3 as 0-convergent non-zero Real_Sequence by A64,
FDIFF_1:def 1;
A65:    N1 c= dom f by A14,A56,XBOOLE_1:1;
A66:    now
          let n;
          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: x1-r<s & s<x1+r} by A67;
          hence x1-r/(n+2) in N1 by A58,RCOMP_1:def 2;
        end;
A68:    rng (h2+c) c= N1
        proof
          let y;
          assume y in rng (h2+c);
          then consider n 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 thesis by A66;
        end;
A70:    now
          let n;
          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: x1-r<s & s<x1+r} by A71;
          hence x1+r/(n+2) in N1 by A58,RCOMP_1:def 2;
        end;
A72:    rng (h1+c) c= N1
        proof
          let y;
          assume y in rng (h1+c);
          then consider n 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 thesis by A70;
        end;
A74:    now
          let n;
          0<r/(n+2) by A57,XREAL_1:139;
          hence 0<s2.n by A59;
        end;
A75:    for n holds (h1"(#)(f/*(h1+c) - f/*c)).n <= 0
        proof
          let n;
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
            let n1;
            (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;
          end;
          then
A78:      rng (h1+c) c= ].p,g.[ by FUNCT_2:114;
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 thesis by A77,A76;
        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
          let n;
          0<r/(n+2) by A57,XREAL_1:139;
          then -(r/(n+2))<-0 by XREAL_1:24;
          hence s3.n<0 by A63;
        end;
A83:    for n holds 0 <= (h2"(#)(f/*(h2+c) - f/*c)).n
        proof
          let n;
          now
            let n1;
            (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;
          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;
          (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 thesis by A86,A85;
        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;
      end;
    end;
    hence thesis;
  end;
end;

::$N Rolle Theorem
theorem
  for x,t st 0<t for f st [.x,x+t.] c= dom f & f|[.x,x+t.] is continuous
& f.x=f.(x+t) & f is_differentiable_on ].x,x+t.[ ex s st 0<s & s<1 & diff(f,x+s
  *t)=0
proof
  let x,t such that
A1: 0<t;
  let f;
  assume [.x,x+t.] c= dom f & f|[.x,x+t.] is continuous & f.x=f.(x+t) & f
  is_differentiable_on ].x,x+t.[;
  then consider x0 such that
A2: x0 in ].x,x+t.[ and
A3: diff(f,x0)=0 by A1,Th1,XREAL_1:29;
  take s = (x0-x)/t;
  x0 in {r: x<r & r<x+t} by A2,RCOMP_1:def 2;
  then
A4: ex g st g=x0 & x<g & g<x+t;
  then 0<x0-x by XREAL_1:50;
  then 0/t < (x0-x)/t by A1,XREAL_1:74;
  hence 0<s;
  x0-x<t by A4,XREAL_1:19;
  then (x0-x)/t<t/t by A1,XREAL_1:74;
  hence s<1 by A1,XCMPLX_1:60;
  s*t+x = (x0-x)+x by A1,XCMPLX_1:87;
  hence thesis by A3;
end;

::$N The Mean Value Theorem
theorem Th3:
  for p,g st p<g for f st [.p,g.] c= dom f & f|[.p,g.] is
continuous & f is_differentiable_on ].p,g.[ ex x0 st x0 in ].p,g.[ & diff(f,x0)
  =(f.g-f.p)/(g-p)
proof
  let p,g such that
A1: p<g;
A2: 0<>g-p by A1;
  reconsider Z=].p,g.[ as open Subset of REAL;
  defpred P[set] means $1 in [.p,g.];
  let f such that
A3: [.p,g.] c= dom f and
A4: f|[.p,g.] is continuous and
A5: f is_differentiable_on ].p,g.[;
  set r = (f.g-f.p)/(g-p);
  deffunc F(Real) =r*($1-p);
  consider f1 such that
A6: (for x holds x in dom f1 iff P[x]) & for x st x in dom f1 holds f1.
  x = F(x) from SEQ_1:sch 3;
  set f2 = f - f1;
A7: [.p,g.] c= dom f1
  proof
    let y;
    assume y in [.p,g.];
    hence thesis by A6;
  end;
  then
A8: [.p,g.] c= dom f /\ dom f1 by A3,XBOOLE_1:19;
  then
A9: [.p,g.] c= dom f2 by VALUED_1:12;
  [.p,g.] = ].p,g.[ \/ {p,g} by A1,XXREAL_1:128;
  then
A10: {p,g} c= [.p,g.] by XBOOLE_1:7;
  then
A11: p in [.p,g.] by ZFMISC_1:32;
  then
A12: p in dom f1 by A6;
  [.p,g.] c= dom f /\ dom f1 by A3,A7,XBOOLE_1:19;
  then
A13: [.p,g.] c= dom f2 by VALUED_1:12;
  then
A14: f2.p = f.p-f1.p by A11,VALUED_1:13
    .= f.p - r*(p-p) by A6,A12
    .= f.p;
A15: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
  then
A16: Z c= dom f1 by A7,XBOOLE_1:1;
A17: now
    let x;
    assume x in Z;
    then x in dom f1 by A15,A6;
    hence f1.x = r*(x-p) by A6
      .= r*x + -r*p;
  end;
  then
A18: f1 is_differentiable_on Z by A16,FDIFF_1:23;
  now
    let x be real number;
    assume x in [.p,g.];
    then x in dom f1 by A6;
    hence f1.x = r*(x-p) by A6
      .= r*x + -r*p;
  end;
  then f1|[.p,g.] is continuous by FCONT_1:41;
  then
A19: f2|[.p,g.] is continuous by A4,A8,FCONT_1:18;
A20: g in [.p,g.] by A10,ZFMISC_1:32;
  then
A21: g in dom f1 by A6;
  Z c= dom f by A3,A15,XBOOLE_1:1;
  then Z c= dom f /\ dom f1 by A16,XBOOLE_1:19;
  then
A22: Z c= dom f2 by VALUED_1:12;
  f2.g = f.g-f1.g by A20,A13,VALUED_1:13
    .= f.g - ((f.g-f.p)/(g-p))*(g-p) by A6,A21
    .= f.g - (f.g-f.p) by A2,XCMPLX_1:87
    .= f2.p by A14;
  then consider x0 such that
A23: x0 in ].p,g.[ and
A24: diff(f2,x0)=0 by A1,A5,A18,A9,A19,A22,Th1,FDIFF_1:19;
  take x0;
  f2 is_differentiable_on Z by A5,A18,A22,FDIFF_1:19;
  then diff(f2,x0) = (f2`|Z).x0 by A23,FDIFF_1:def 7
    .= diff(f,x0) - diff(f1,x0) by A5,A18,A22,A23,FDIFF_1:19
    .= diff(f,x0) - (f1`|Z).x0 by A18,A23,FDIFF_1:def 7;
  hence thesis by A16,A17,A23,A24,FDIFF_1:23;
end;

::$N Lagrange Theorem
theorem
  for x,t st 0<t for f st [.x,x+t.] c= dom f & f|[.x,x+t.] is continuous
& f is_differentiable_on ].x,x+t.[ ex s st 0<s & s<1 & f.(x+t) = f.x + t*diff(f
  ,x+s*t)
proof
  let x,t such that
A1: 0<t;
  let f;
  assume [.x,x+t.] c= dom f & f|[.x,x+t.] is continuous & f
  is_differentiable_on ].x,x+t.[;
  then consider x0 such that
A2: x0 in ].x,x+t.[ and
A3: diff(f,x0)=(f.(x+t)-f.x)/(x+t-x) by A1,Th3,XREAL_1:29;
  take s = (x0-x)/t;
  x0 in {r: x<r & r<x+t} by A2,RCOMP_1:def 2;
  then
A4: ex g st g=x0 & x<g & g<x+t;
  then 0<x0-x by XREAL_1:50;
  then 0/t < (x0-x)/t by A1,XREAL_1:74;
  hence 0<s;
  x0-x<t by A4,XREAL_1:19;
  then (x0-x)/t<t/t by A1,XREAL_1:74;
  hence s<1 by A1,XCMPLX_1:60;
A5: s*t+x = (x0-x)+x by A1,XCMPLX_1:87;
  f.x + t*diff(f,x0)=f.x + (f.(x+t)-f.x) by A1,A3,XCMPLX_1:87;
  hence thesis by A5;
end;

theorem Th5:
  for p,g st p<g for f1,f2 st [.p,g.] c= dom f1 & [.p,g.] c= dom f2
  & f1|[.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2|[.p,g.] is
continuous & f2 is_differentiable_on ].p,g.[ ex x0 st x0 in ].p,g.[ & (f1.g-f1.
  p)*diff(f2,x0)=(f2.g-f2.p)*diff(f1,x0)
proof
  let p,g such that
A1: p<g;
  let f1,f2 such that
A2: [.p,g.] c= dom f1 and
A3: [.p,g.] c= dom f2 and
A4: f1|[.p,g.] is continuous and
A5: f1 is_differentiable_on ].p,g.[ and
A6: f2|[.p,g.] is continuous and
A7: f2 is_differentiable_on ].p,g.[;
A8: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
  now
    per cases;
    suppose
A9:   f2.p=f2.g;
      then consider x0 such that
A10:  x0 in ].p,g.[ & diff(f2,x0) = 0 by A1,A3,A6,A7,Th1;
      take x0;
      thus x0 in ].p,g.[ & (f1.g-f1.p)*diff(f2,x0)=(f2.g-f2.p)*diff(f1,x0) by
A9,A10;
    end;
    suppose
      f2.p<>f2.g;
      then
A11:  f2.g-f2.p<>0;
      reconsider Z=].p,g.[ as open Subset of REAL;
      set s=(f1.g-f1.p)/(f2.g-f2.p);
      reconsider f3 = [.p,g.] --> f1.p - f2.p*s as PartFunc of [.p,g.], REAL
      by FUNCOP_1:45;
      reconsider f3 as PartFunc of REAL, REAL;
      set f4 = s(#)f2;
      set f5 = f3+f4;
      set f=f5-f1;
A12:  Z c= dom f3 by A8,FUNCOP_1:13;
A13:  dom f4 = dom f2 by VALUED_1:def 5;
      then
A14:  Z c= dom f4 by A3,A8,XBOOLE_1:1;
      then Z c= dom f3 /\ dom f4 by A12,XBOOLE_1:19;
      then
A15:  Z c= dom f5 by VALUED_1:def 1;
A16:  [.p,g.] = dom f3 by FUNCOP_1:13;
      then for x st x in [.p,g.] /\ dom f3 holds f3.x=f1.p - f2.p*s by
FUNCOP_1:7;
      then
A17:  f3|[.p,g.] is constant by PARTFUN2:57;
      then
A18:  f3|].p,g.[ is constant by PARTFUN2:38,XXREAL_1:25;
      then
A19:  f3 is_differentiable_on Z by A12,FDIFF_1:22;
A20:  p in [.p,g.] by A1,XXREAL_1:1;
      then p in dom f3 /\ dom f4 by A3,A16,A13,XBOOLE_0:def 4;
      then
A21:  p in dom f5 by VALUED_1:def 1;
      then p in dom f5 /\ dom f1 by A2,A20,XBOOLE_0:def 4;
      then p in dom f by VALUED_1:12;
      then
A22:  f.p = f5.p - f1.p by VALUED_1:13
        .= f3.p + f4.p - f1.p by A21,VALUED_1:def 1
        .= f3.p + s*f2.p - f1.p by A3,A13,A20,VALUED_1:def 5
        .= f1.p - s*f2.p + s*f2.p - f1.p by A20,FUNCOP_1:7
        .= 0;
A23:  g in [.p,g.] by A1,XXREAL_1:1;
      then g in dom f3 /\ dom f4 by A3,A16,A13,XBOOLE_0:def 4;
      then
A24:  g in dom f5 by VALUED_1:def 1;
      then g in dom f5 /\ dom f1 by A2,A23,XBOOLE_0:def 4;
      then g in dom f by VALUED_1:12;
      then
A25:  f.g = f5.g - f1.g by VALUED_1:13
        .= f3.g + f4.g - f1.g by A24,VALUED_1:def 1
        .= f3.g + s*f2.g - f1.g by A3,A13,A23,VALUED_1:def 5
        .= f1.p - s*f2.p + s*f2.g - f1.g by A23,FUNCOP_1:7
        .= -f1.g+(f1.p-(-(f1.g-f1.p))/(f2.g-f2.p)*(f2.g-f2.p))
        .= -f1.g+(f1.p-(f1.p-f1.g)) by A11,XCMPLX_1:87
        .= f.p by A22;
      Z c= dom f1 by A2,A8,XBOOLE_1:1;
      then Z c= dom f5 /\ dom f1 by A15,XBOOLE_1:19;
      then
A26:  Z c= dom f by VALUED_1:12;
      dom f4 = dom f2 by VALUED_1:def 5;
      then
A27:  [.p,g.] c= dom f3 /\ dom f4 by A3,A16,XBOOLE_1:19;
      then [.p,g.] c= dom f5 by VALUED_1:def 1;
      then
A28:  [.p,g.] c= dom f5 /\ dom f1 by A2,XBOOLE_1:19;
      f4|[.p,g.] is continuous by A3,A6,FCONT_1:20;
      then f5|[.p,g.] is continuous by A17,A27,FCONT_1:18;
      then
A29:  f|[.p,g.] is continuous by A4,A28,FCONT_1:18;
A30:  f4 is_differentiable_on Z by A7,A14,FDIFF_1:20;
      then
A31:  f5 is_differentiable_on Z by A19,A15,FDIFF_1:18;
      [.p,g.] c= dom f by A28,VALUED_1:12;
      then consider x0 such that
A32:  x0 in ].p,g.[ and
A33:  diff(f,x0)=0 by A1,A5,A29,A31,A26,A25,Th1,FDIFF_1:19;
      take x0;
      f is_differentiable_on Z by A5,A31,A26,FDIFF_1:19;
      then diff(f,x0) = (f`|Z).x0 by A32,FDIFF_1:def 7
        .= diff(f5,x0) - diff(f1,x0) by A5,A31,A26,A32,FDIFF_1:19
        .= (f5`|Z).x0 - diff(f1,x0) by A31,A32,FDIFF_1:def 7
        .= diff(f3,x0) + diff(f4,x0) - diff(f1,x0) by A19,A30,A15,A32,
FDIFF_1:18
        .= (f3`|Z).x0 + diff(f4,x0) - diff(f1,x0) by A19,A32,FDIFF_1:def 7
        .= 0 + diff(f4,x0) - diff(f1,x0) by A18,A12,A32,FDIFF_1:22
        .= (f4`|Z).x0 - diff(f1,x0) by A30,A32,FDIFF_1:def 7
        .= s*diff(f2,x0) - diff(f1,x0) by A7,A14,A32,FDIFF_1:20;
      then
      (diff(f2,x0)*(f1.g-f1.p))/(f2.g-f2.p)*(f2.g-f2.p) = diff(f1,x0)*(f2
      .g-f2.p) by A33,XCMPLX_1:15;
      hence x0 in ].p,g.[ & (f1.g-f1.p)*diff(f2,x0) = (f2.g-f2.p)*diff(f1,x0)
      by A11,A32,XCMPLX_1:87;
    end;
  end;
  hence thesis;
end;

::$N Cauchy Theorem
theorem
  for x,t st 0<t for f1,f2 st [.x,x+t.] c= dom f1 & [.x,x+t.] c= dom f2
& f1|[.x,x+t.] is continuous & f1 is_differentiable_on ].x,x+t.[ & f2|[.x,x+t.]
is continuous & f2 is_differentiable_on ].x,x+t.[ & (for x1 st x1 in ].x,x+t.[
  holds diff(f2,x1)<>0) ex s st 0<s & s<1 & (f1.(x+t)-f1.x)/(f2.(x+t)-f2.x) =
  diff(f1,x+s*t)/diff(f2,x+s*t)
proof
  let x,t such that
A1: 0<t;
  let f1,f2 such that
A2: [.x,x+t.] c= dom f1 and
A3: [.x,x+t.] c= dom f2 and
A4: f1|[.x,x+t.] is continuous & f1 is_differentiable_on ].x,x+t.[ and
A5: f2|[.x,x+t.] is continuous & f2 is_differentiable_on ].x,x+t.[ and
A6: for x1 st x1 in ].x,x+t.[ holds diff(f2,x1)<>0;
  consider x0 such that
A7: x0 in ].x,x+t.[ and
A8: (f1.(x+t)-f1.x)*diff(f2,x0)=(f2.(x+t)-f2.x)*diff(f1,x0) by A1,A2,A3,A4,A5
,Th5,XREAL_1:29;
  diff(f2,x0)*((f1.(x+t)-f1.x)/diff(f2, x0))= (f2.(x+t)-f2.x)*diff(f1,x0)
  /diff(f2,x0) by A8,XCMPLX_1:74;
  then
  (f1.(x+t)-f1.x)/(f2.(x+t)-f2.x) = (f2.(x+t)-f2.x)* (diff(f1,x0)/diff(f2
  ,x0))/(f2.(x+t)-f2.x) by A6,A7,XCMPLX_1:87;
  then
A9: (f1.(x+t)-f1.x)/(f2.(x+t)-f2.x)=((diff(f1,x0)/diff(f2,x0))/(f2.(x+t) -
  f2.x))* (f2.(x+t)-f2.x);
  take s = (x0-x)/t;
  x0 in {r: x<r & r<x+t} by A7,RCOMP_1:def 2;
  then
A10: ex g st g=x0 & x<g & g<x+t;
  then 0<x0-x by XREAL_1:50;
  then 0/t < (x0-x)/t by A1,XREAL_1:74;
  hence 0<s;
  x0-x<t by A10,XREAL_1:19;
  then (x0-x)/t<t/t by A1,XREAL_1:74;
  hence s<1 by A1,XCMPLX_1:60;
A11: s*t+x = (x0-x)+x by A1,XCMPLX_1:87;
  0<>f2.(x+t)-f2.x by A1,A3,A5,A6,Th1,XREAL_1:29;
  hence thesis by A9,A11,XCMPLX_1:87;
end;

theorem Th7:
  for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g
  .[ & (for x st x in ].p,g.[ holds diff(f,x) = 0) holds f|].p,g.[ is constant
proof
  let p,g;
  let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds diff(f,x) = 0;
  now
    let x1,x2;
    assume x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f;
    then
A4: x1 in ].p,g.[ & x2 in ].p,g.[ by XBOOLE_0:def 4;
    now
      per cases;
      suppose
        x1=x2;
        hence f.x1=f.x2;
      end;
      suppose
A5:     not x1=x2;
        now
          per cases by A5,XXREAL_0:1;
          suppose
A6:         x1<x2;
            then 0<>x2-x1;
            then
A7:         0<>(x2-x1)" by XCMPLX_1:202;
            reconsider Z=].x1,x2.[ as open Subset of REAL;
A8:         [.x1,x2.] c= ].p,g.[ by A4,XXREAL_2:def 12;
            f|].p,g.[ is continuous by A2,FDIFF_1:25;
            then
A9:         f|[.x1,x2.] is continuous by A8,FCONT_1:16;
A10:        Z c= [.x1,x2.] by XXREAL_1:25;
            then f is_differentiable_on Z by A2,A8,FDIFF_1:26,XBOOLE_1:1;
            then
A11:        ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1)
            by A1,A6,A8,A9,Th3,XBOOLE_1:1;
            Z c= ].p,g.[ by A8,A10,XBOOLE_1:1;
            then 0 = (f.x2-f.x1) by A3,A7,A11,XCMPLX_1:6;
            hence f.x1=f.x2;
          end;
          suppose
A12:        x2<x1;
            then 0<>x1-x2;
            then
A13:        0<>(x1-x2)" by XCMPLX_1:202;
            reconsider Z=].x2,x1.[ as open Subset of REAL;
A14:        [.x2,x1.] c= ].p,g.[ by A4,XXREAL_2:def 12;
            f|].p,g.[ is continuous by A2,FDIFF_1:25;
            then
A15:        f|[.x2,x1.] is continuous by A14,FCONT_1:16;
A16:        Z c= [.x2,x1.] by XXREAL_1:25;
            then f is_differentiable_on Z by A2,A14,FDIFF_1:26,XBOOLE_1:1;
            then
A17:        ex x0 st x0 in ].x2,x1.[ & diff(f,x0) = (f.x1-f.x2)/(x1- x2)
            by A1,A12,A14,A15,Th3,XBOOLE_1:1;
            Z c= ].p,g.[ by A14,A16,XBOOLE_1:1;
            then 0 = (f.x1-f.x2) by A3,A13,A17,XCMPLX_1:6;
            hence f.x1=f.x2;
          end;
        end;
        hence f.x1=f.x2;
      end;
    end;
    hence f.x1=f.x2;
  end;
  hence thesis by PARTFUN2:58;
end;

theorem
  for p,g for f1,f2 st f1 is_differentiable_on ].p,g.[ & f2
is_differentiable_on ].p,g.[ & (for x st x in ].p,g.[ holds diff(f1,x) = diff(
f2,x)) holds (f1-f2)|].p,g.[ is constant & ex r st for x st x in ].p,g.[ holds
  f1.x = f2.x+r
proof
  let p,g;
  let f1,f2 such that
A1: f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ and
A2: for x st x in ].p,g.[ holds diff(f1,x) = diff(f2,x);
  reconsider Z=].p,g.[ as open Subset of REAL;
  ].p,g.[ c= dom f1 & ].p,g.[ c= dom f2 by A1,FDIFF_1:def 6;
  then ].p,g.[ c= dom f1 /\ dom f2 by XBOOLE_1:19;
  then
A3: ].p,g.[ c= dom (f1-f2) by VALUED_1:12;
  then
A4: f1-f2 is_differentiable_on Z by A1,FDIFF_1:19;
  now
    let x;
    assume
A5: x in ].p,g.[;
    hence diff(f1-f2,x) = ((f1-f2)`|Z).x by A4,FDIFF_1:def 7
      .= diff(f1,x)-diff(f2,x) by A1,A3,A5,FDIFF_1:19
      .= diff(f1,x)-diff(f1,x) by A2,A5
      .= 0;
  end;
  hence (f1-f2)|].p,g.[ is constant by A1,A3,Th7,FDIFF_1:19;
  then consider r such that
A6: for x st x in ].p,g.[ /\ dom(f1-f2) holds (f1-f2).x = r by PARTFUN2:57;
  take r;
  let x;
  assume
A7: x in ].p,g.[;
  then x in ].p,g.[ /\ dom(f1-f2) by A3,XBOOLE_1:28;
  then r = (f1-f2).x by A6
    .= f1.x - f2.x by A3,A7,VALUED_1:13;
  hence thesis;
end;

theorem
  for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & (
  for x st x in ].p,g.[ holds 0<diff(f,x)) holds f|].p,g.[ is increasing
proof
  let p,g;
  let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds 0<diff(f,x);
  now
    let x1,x2 such that
A4: x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f and
A5: x1<x2;
A6: 0<x2-x1 by A5,XREAL_1:50;
    reconsider Z=].x1,x2.[ as open Subset of REAL;
    x1 in ].p,g.[ & x2 in ].p,g.[ by A4,XBOOLE_0:def 4;
    then
A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def 12;
    f|].p,g.[ is continuous by A2,FDIFF_1:25;
    then
A8: f|[.x1,x2.] is continuous by A7,FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
    then f is_differentiable_on Z by A2,A7,FDIFF_1:26,XBOOLE_1:1;
    then
A10: ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1) by A1,A5,A7
,A8,Th3,XBOOLE_1:1;
    Z c= ].p,g.[ by A7,A9,XBOOLE_1:1;
    then 0<f.x2-f.x1 by A3,A6,A10;
    then f.x1+0<f.x2 by XREAL_1:20;
    hence f.x1<f.x2;
  end;
  hence thesis by RFUNCT_2:20;
end;

theorem
  for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & (
  for x st x in ].p,g.[ holds diff(f,x)<0) holds f|].p,g.[ is decreasing
proof
  let p,g;
  let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds diff(f,x)<0;
  now
    let x1,x2 such that
A4: x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f and
A5: x1<x2;
A6: 0<x2-x1 by A5,XREAL_1:50;
    reconsider Z=].x1,x2.[ as open Subset of REAL;
    x1 in ].p,g.[ & x2 in ].p,g.[ by A4,XBOOLE_0:def 4;
    then
A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def 12;
    f|].p,g.[ is continuous by A2,FDIFF_1:25;
    then
A8: f|[.x1,x2.] is continuous by A7,FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
    then f is_differentiable_on Z by A2,A7,FDIFF_1:26,XBOOLE_1:1;
    then
A10: ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1) by A1,A5,A7
,A8,Th3,XBOOLE_1:1;
    Z c= ].p,g.[ by A7,A9,XBOOLE_1:1;
    then f.x2-f.x1<0 by A3,A6,A10;
    then f.x2<f.x1+0 by XREAL_1:19;
    hence f.x2<f.x1;
  end;
  hence thesis by RFUNCT_2:21;
end;

theorem
  for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & (
  for x st x in ].p,g.[ holds 0<=diff(f,x)) holds f|].p,g.[ is non-decreasing
proof
  let p,g;
  let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds 0<=diff(f,x);
  now
    let x1,x2 such that
A4: x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f and
A5: x1<x2;
A6: 0<>x2-x1 by A5;
    reconsider Z=].x1,x2.[ as open Subset of REAL;
    x1 in ].p,g.[ & x2 in ].p,g.[ by A4,XBOOLE_0:def 4;
    then
A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def 12;
    f|].p,g.[ is continuous by A2,FDIFF_1:25;
    then
A8: f|[.x1,x2.] is continuous by A7,FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
    then
A10: Z c= ].p,g.[ by A7,XBOOLE_1:1;
    f is_differentiable_on Z by A2,A7,A9,FDIFF_1:26,XBOOLE_1:1;
    then
    ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1) by A1,A5,A7,A8
,Th3,XBOOLE_1:1;
    then
A11: 0<=(f.x2-f.x1)/(x2-x1) by A3,A10;
    0<=x2-x1 by A5,XREAL_1:50;
    then 0*(x2-x1)<=(f.x2-f.x1)/(x2-x1)*(x2-x1) by A11;
    then 0<=f.x2-f.x1 by A6,XCMPLX_1:87;
    then f.x1+0<=f.x2 by XREAL_1:19;
    hence f.x1<=f.x2;
  end;
  hence thesis by RFUNCT_2:22;
end;

theorem
  for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & (
  for x st x in ].p,g.[ holds diff(f,x)<=0) holds f|].p,g.[ is non-increasing
proof
  let p,g;
  let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds diff(f,x)<=0;
  now
    let x1,x2 such that
A4: x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f and
A5: x1<x2;
A6: 0<=x2-x1 by A5,XREAL_1:50;
    reconsider Z=].x1,x2.[ as open Subset of REAL;
    x1 in ].p,g.[ & x2 in ].p,g.[ by A4,XBOOLE_0:def 4;
    then
A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def 12;
    f|].p,g.[ is continuous by A2,FDIFF_1:25;
    then
A8: f|[.x1,x2.] is continuous by A7,FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
    then f is_differentiable_on Z by A2,A7,FDIFF_1:26,XBOOLE_1:1;
    then
A10: ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1) by A1,A5,A7
,A8,Th3,XBOOLE_1:1;
A11: 0<>x2-x1 by A5;
    Z c= ].p,g.[ by A7,A9,XBOOLE_1:1;
    then (f.x2-f.x1)/(x2-x1)*(x2-x1)<=0*(x2-x1) by A3,A6,A10,XREAL_1:64;
    then f.x2-f.x1<=0 by A11,XCMPLX_1:87;
    then f.x2<=f.x1+0 by XREAL_1:20;
    hence f.x2<=f.x1;
  end;
  hence thesis by RFUNCT_2:23;
end;