rolle.miz



    begin

    reserve y for set;

    reserve g,r,s,p,t,x,x0,x1,x2 for Real;

    reserve n,n1 for Nat;

    reserve s1,s2,s3 for Real_Sequence;

    reserve f,f1,f2 for PartFunc of REAL , REAL ;

    theorem :: ROLLE:1

    

     Th1: for p, g st p < g holds for f st [.p, g.] c= ( dom f) & (f | [.p, g.]) is continuous & (f . p) = (f . g) & f is_differentiable_on ].p, g.[ holds 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 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 Element of 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;

      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 such that

             A24: 0 < r and

             A25: N1 = ].(x2 - r), (x2 + r).[ by RCOMP_1:def 6;

            reconsider r as Real;

            deffunc F( 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( 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;

             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 be object;

              assume y in ( rng (h2 + c));

              then

              consider n be 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 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 be object;

              assume y in ( rng (h1 + c));

              then

              consider n be 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 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;

              reconsider n as Element of NAT by ORDINAL1:def 12;

              now

                let n1 be Element of NAT ;

                ((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 be Element of NAT ;

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

              reconsider 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 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 such that

             A57: 0 < r and

             A58: N1 = ].(x1 - r), (x1 + r).[ by RCOMP_1:def 6;

            reconsider r as Real;

            deffunc F( 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( 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;

             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 be object;

              assume y in ( rng (h2 + c));

              then

              consider n be 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 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 be object;

              assume y in ( rng (h1 + c));

              then

              consider n be 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 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 be Element of NAT ;

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

              reconsider 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 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 be Element of NAT ;

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

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

    ::$Notion-Name

    theorem :: ROLLE:2

    for x, t st 0 < t holds 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).[ holds 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;

    ::$Notion-Name

    theorem :: ROLLE:3

    

     Th3: for p, g st p < g holds for f st [.p, g.] c= ( dom f) & (f | [.p, g.]) is continuous & f is_differentiable_on ].p, g.[ holds 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) = ( In ((r * ($1 - p)), REAL ));

      consider f1 such that

       A6: (for x be Element of REAL holds x in ( dom f1) iff P[x]) & for x be Element of REAL st x in ( dom f1) holds (f1 . x) = F(x) from SEQ_1:sch 3;

      

       A7: for x be Real st x in ( dom f1) holds (f1 . x) = (r * (x - p))

      proof

        let x be Real such that

         A8: x in ( dom f1);

        reconsider x as Real;

        (f1 . x) = F(x) by A6, A8;

        hence thesis;

      end;

      set f2 = (f - f1);

      

       A9: [.p, g.] c= ( dom f1) by A6;

      then

       A10: [.p, g.] c= (( dom f) /\ ( dom f1)) by A3, XBOOLE_1: 19;

      then

       A11: [.p, g.] c= ( dom f2) by VALUED_1: 12;

       [.p, g.] = ( ].p, g.[ \/ {p, g}) by A1, XXREAL_1: 128;

      then

       A12: {p, g} c= [.p, g.] by XBOOLE_1: 7;

      then

       A13: p in [.p, g.] by ZFMISC_1: 32;

      then

       A14: p in ( dom f1) by A6;

       [.p, g.] c= (( dom f) /\ ( dom f1)) by A3, A9, XBOOLE_1: 19;

      then

       A15: [.p, g.] c= ( dom f2) by VALUED_1: 12;

      

      then

       A16: (f2 . p) = ((f . p) - (f1 . p)) by A13, VALUED_1: 13

      .= ((f . p) - (r * (p - p))) by A14, A7

      .= (f . p);

      

       A17: ].p, g.[ c= [.p, g.] by XXREAL_1: 25;

      then

       A18: Z c= ( dom f1) by A9;

       A19:

      now

        let x;

        assume x in Z;

        then x in ( dom f1) by A17, A6;

        

        hence (f1 . x) = (r * (x - p)) by A7

        .= ((r * x) + ( - (r * p)));

      end;

      then

       A20: f1 is_differentiable_on Z by A18, FDIFF_1: 23;

      now

        let x be Real;

        assume x in [.p, g.];

        then x in ( dom f1) by A6;

        

        hence (f1 . x) = (r * (x - p)) by A7

        .= ((r * x) + ( - (r * p)));

      end;

      then (f1 | [.p, g.]) is continuous by FCONT_1: 41;

      then

       A21: (f2 | [.p, g.]) is continuous by A4, A10, FCONT_1: 18;

      

       A22: g in [.p, g.] by A12, ZFMISC_1: 32;

      then

       A23: g in ( dom f1) by A6;

      Z c= ( dom f) by A3, A17;

      then Z c= (( dom f) /\ ( dom f1)) by A18, XBOOLE_1: 19;

      then

       A24: Z c= ( dom f2) by VALUED_1: 12;

      (f2 . g) = ((f . g) - (f1 . g)) by A22, A15, VALUED_1: 13

      .= ((f . g) - ((((f . g) - (f . p)) / (g - p)) * (g - p))) by A7, A23

      .= ((f . g) - ((f . g) - (f . p))) by A2, XCMPLX_1: 87

      .= (f2 . p) by A16;

      then

      consider x0 such that

       A25: x0 in ].p, g.[ and

       A26: ( diff (f2,x0)) = 0 by A1, A5, A20, A11, A21, A24, Th1, FDIFF_1: 19;

      take x0;

      f2 is_differentiable_on Z by A5, A20, A24, FDIFF_1: 19;

      

      then ( diff (f2,x0)) = ((f2 `| Z) . x0) by A25, FDIFF_1:def 7

      .= (( diff (f,x0)) - ( diff (f1,x0))) by A5, A20, A24, A25, FDIFF_1: 19

      .= (( diff (f,x0)) - ((f1 `| Z) . x0)) by A20, A25, FDIFF_1:def 7;

      hence thesis by A18, A19, A25, A26, FDIFF_1: 23;

    end;

    ::$Notion-Name

    theorem :: ROLLE:4

    for x, t st 0 < t holds for f st [.x, (x + t).] c= ( dom f) & (f | [.x, (x + t).]) is continuous & f is_differentiable_on ].x, (x + t).[ holds 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 :: ROLLE:5

    

     Th5: for p, g st p < g holds 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.[ holds 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 fp = ((f1 . p) - ((f2 . p) * s)) as Element of REAL by XREAL_0:def 1;

          reconsider f3 = ( [.p, g.] --> fp) 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;

          then Z c= (( dom f3) /\ ( dom f4)) by A12, XBOOLE_1: 19;

          then

           A15: Z c= ( dom f5) by VALUED_1:def 1;

          reconsider f1pf2p = ((f1 . p) - ((f2 . p) * s)) as Element of REAL by XREAL_0:def 1;

          

           A16: [.p, g.] = ( dom f3) by FUNCOP_1: 13;

          then for x be Element of REAL st x in ( [.p, g.] /\ ( dom f3)) holds (f3 . x) = f1pf2p 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;

          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;

    ::$Notion-Name

    theorem :: ROLLE:6

    for x, t st 0 < t holds 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 ) holds 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 :: ROLLE:7

    

     Th7: for p, g holds 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 be Element of REAL ;

        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;

                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;

                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 :: ROLLE:8

    for p, g holds 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 be Element of REAL such that

       A6: for x be Element of REAL 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 :: ROLLE:9

    for p, g holds 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;

        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 :: ROLLE:10

    for p, g holds 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;

        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 :: ROLLE:11

    for p, g holds 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;

        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 :: ROLLE:12

    for p, g holds 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;

        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;