taylor_1.miz



    begin

    reserve n for Nat,

i for Integer,

p,x,x0,y for Real,

q for Rational,

f for PartFunc of REAL , REAL ;

    definition

      let q be Integer;

      :: TAYLOR_1:def1

      func #Z q -> Function of REAL , REAL means

      : Def1: for x be Real holds (it . x) = (x #Z q);

      existence

      proof

        deffunc U( Real) = ( In (($1 #Z q), REAL ));

        consider f be Function of REAL , REAL such that

         A1: for d be Element of REAL holds (f . d) = U(d) from FUNCT_2:sch 4;

        take f;

        let d be Real;

        d in REAL by XREAL_0:def 1;

        then (f . d) = U(d) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of REAL , REAL ;

        assume that

         A2: for d be Real holds (f1 . d) = (d #Z q) and

         A3: for d be Real holds (f2 . d) = (d #Z q);

        for d be Element of REAL holds (f1 . d) = (f2 . d)

        proof

          let d be Element of REAL ;

          

          thus (f1 . d) = (d #Z q) by A2

          .= (f2 . d) by A3;

        end;

        hence f1 = f2;

      end;

    end

    theorem :: TAYLOR_1:1

    

     Th1: for m,n be Nat holds (x #Z (n + m)) = ((x #Z n) * (x #Z m))

    proof

      let m,n be Nat;

      per cases ;

        suppose x <> 0 ;

        hence thesis by PREPOWER: 44;

      end;

        suppose

         A1: x = 0 ;

        thus thesis

        proof

          

           A2: ( 0 #Z (n + m)) = ( 0 |^ |.(n + m).|) by PREPOWER:def 3

          .= ( 0 |^ (n + m)) by ABSVALUE:def 1

          .= (( 0 |^ n) * ( 0 |^ m)) by NEWTON: 8;

          per cases ;

            suppose

             A3: n = 0 & m = 0 ;

            (x #Z ( 0 + 0 )) = (1 * (x #Z 0 ))

            .= ((x #Z 0 ) * (x #Z 0 )) by PREPOWER: 34;

            hence thesis by A3;

          end;

            suppose n <> 0 ;

            then

             A4: ( 0 + 1) <= n by NAT_1: 13;

            

             A5: (( 0 #Z n) * ( 0 #Z m)) = (( 0 |^ |.n.|) * ( 0 #Z m)) by PREPOWER:def 3

            .= (( 0 |^ n) * ( 0 #Z m)) by ABSVALUE:def 1

            .= ( 0 * ( 0 #Z m)) by A4, NEWTON: 11;

            ( 0 #Z (n + m)) = ( 0 * ( 0 |^ m)) by A2, A4, NEWTON: 11;

            hence thesis by A1, A5;

          end;

            suppose m <> 0 ;

            then

             A6: ( 0 + 1) <= m by NAT_1: 13;

            

             A7: (( 0 #Z n) * ( 0 #Z m)) = (( 0 |^ |.m.|) * ( 0 #Z n)) by PREPOWER:def 3

            .= (( 0 |^ m) * ( 0 #Z n)) by ABSVALUE:def 1

            .= ( 0 * ( 0 #Z n)) by A6, NEWTON: 11;

            ( 0 #Z (n + m)) = ( 0 * ( 0 |^ n)) by A2, A6, NEWTON: 11;

            hence thesis by A1, A7;

          end;

        end;

      end;

    end;

    theorem :: TAYLOR_1:2

    

     Th2: ( #Z n) is_differentiable_in x & ( diff (( #Z n),x)) = (n * (x #Z (n - 1)))

    proof

      defpred P[ Nat] means for x be Real holds ( #Z $1) is_differentiable_in x & ( diff (( #Z $1),x)) = ($1 * (x #Z ($1 - 1)));

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

         A2:

        now

          let x be Real such that x in REAL ;

          

          thus (( #Z 1) . x) = (x #Z 1) by Def1

          .= ((1 * x) + 0 ) by PREPOWER: 35;

        end;

        

         A3: ( [#] REAL ) is open Subset of REAL ;

        

         A4: REAL c= ( dom ( #Z 1)) by FUNCT_2:def 1;

        then

         A5: ( #Z 1) is_differentiable_on REAL by A2, A3, FDIFF_1: 23;

        

         A6: for x be Real holds ( #Z 1) is_differentiable_in x & ( diff (( #Z 1),x)) = 1

        proof

          let x be Real;

          

           A7: x in REAL by XREAL_0:def 1;

          hence ( #Z 1) is_differentiable_in x by A3, A5, FDIFF_1: 9;

          

          thus ( diff (( #Z 1),x)) = ((( #Z 1) `| REAL ) . x) by A5, A7, FDIFF_1:def 7

          .= 1 by A2, A4, A3, A7, FDIFF_1: 23;

        end;

        let k be Nat such that

         A8: P[k];

        now

          per cases ;

            case

             A9: k = 0 ;

            thus P[(k + 1)]

            proof

              let x be Real;

              thus ( #Z (k + 1)) is_differentiable_in x by A6, A9;

              

              thus ( diff (( #Z (k + 1)),x)) = 1 by A6, A9

              .= ((k + 1) * (x #Z ((k + 1) - 1))) by A9, PREPOWER: 34;

            end;

          end;

            case k <> 0 ;

            then 1 <= k by NAT_1: 14;

            then (1 - 1) <= (k - 1) by XREAL_1: 13;

            then

            reconsider k1 = (k - 1) as Element of NAT by INT_1: 3;

            let x be Real;

            

             A10: REAL = ( dom ( #Z (k + 1))) by FUNCT_2:def 1;

            

             A11: x is Real & ( #Z k) is_differentiable_in x by A8;

            

             A12: for x be object st x in ( dom ( #Z (k + 1))) holds (( #Z (k + 1)) . x) = ((( #Z k) . x) * (( #Z 1) . x))

            proof

              let x be object;

              assume x in ( dom ( #Z (k + 1)));

              then

              reconsider x1 = x as Real;

              

              thus (( #Z (k + 1)) . x) = (x1 #Z (k + 1)) by Def1

              .= ((x1 #Z k) * (x1 #Z 1)) by Th1

              .= ((( #Z k) . x) * (x1 #Z 1)) by Def1

              .= ((( #Z k) . x) * (( #Z 1) . x)) by Def1;

            end;

            

             A13: ( #Z 1) is_differentiable_in x by A6;

            

             A14: (( dom ( #Z k)) /\ ( dom ( #Z 1))) = (( [#] REAL ) /\ ( dom ( #Z 1))) by FUNCT_2:def 1

            .= (( [#] REAL ) /\ REAL ) by FUNCT_2:def 1;

            then ( #Z (k + 1)) = (( #Z k) (#) ( #Z 1)) by A10, A12, VALUED_1:def 4;

            hence ( #Z (k + 1)) is_differentiable_in x by A11, A13, FDIFF_1: 16;

            

            thus ( diff (( #Z (k + 1)),x)) = ( diff ((( #Z k) (#) ( #Z 1)),x)) by A14, A10, A12, VALUED_1:def 4

            .= (((( #Z k) . x) * ( diff (( #Z 1),x))) + (( diff (( #Z k),x)) * (( #Z 1) . x))) by A11, A13, FDIFF_1: 16

            .= (((( #Z k) . x) * 1) + (( diff (( #Z k),x)) * (( #Z 1) . x))) by A6

            .= (((x #Z k) * 1) + (( diff (( #Z k),x)) * (( #Z 1) . x))) by Def1

            .= (((x #Z k) * 1) + (( diff (( #Z k),x)) * (x #Z 1))) by Def1

            .= ((x #Z k) + ((k * (x #Z k1)) * (x #Z 1))) by A8

            .= ((x #Z k) + (k * ((x #Z k1) * (x #Z 1))))

            .= ((x #Z k) + (k * (x #Z (k1 + 1)))) by Th1

            .= ((k + 1) * (x #Z ((k + 1) - 1)));

          end;

        end;

        hence thesis;

      end;

      

       A15: P[ 0 ]

      proof

        let x be Real;

        set f = ( #Z 0 );

        now

          ( dom f) = REAL by FUNCT_2:def 1;

          then

          consider x be object such that

           A16: x in ( dom f) by XBOOLE_0:def 1;

          reconsider x1 = x as Real by A16;

          let y be object such that

           A17: y in {1};

          (f . x) = (x1 #Z 0 ) by Def1

          .= 1 by PREPOWER: 34

          .= y by A17, TARSKI:def 1;

          hence y in ( rng f) by A16, FUNCT_1:def 3;

        end;

        then

         A18: {1} c= ( rng f) by TARSKI:def 3;

        now

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A19: x in ( dom f) and

           A20: y = (f . x) by FUNCT_1:def 3;

          reconsider x as Real by A19;

          (f . x) = (x #Z 0 ) by Def1

          .= 1 by PREPOWER: 34;

          hence y in {1} by A20, TARSKI:def 1;

        end;

        then ( rng f) c= {1} by TARSKI:def 3;

        then

         A21: ( rng f) = {1} by A18, XBOOLE_0:def 10;

        

         A22: ( dom f) = ( [#] REAL ) by FUNCT_2:def 1;

        then

         A23: f is_differentiable_on ( dom f) by A21, FDIFF_1: 11;

        

         A24: x in REAL by XREAL_0:def 1;

        then ((f `| ( dom f)) . x) = 0 by A21, A22, FDIFF_1: 11;

        hence f is_differentiable_in x & ( diff (f,x)) = ( 0 * (x #Z ( 0 - 1))) by A24, A23, A22, FDIFF_1: 9, FDIFF_1:def 7;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A15, A1);

      hence thesis;

    end;

    theorem :: TAYLOR_1:3

    f is_differentiable_in x0 implies (( #Z n) * f) is_differentiable_in x0 & ( diff ((( #Z n) * f),x0)) = ((n * ((f . x0) #Z (n - 1))) * ( diff (f,x0)))

    proof

      assume

       A1: f is_differentiable_in x0;

      

       A2: ( #Z n) is_differentiable_in (f . x0) & x0 is Real by Th2;

      hence (( #Z n) * f) is_differentiable_in x0 by A1, FDIFF_2: 13;

      

      thus ( diff ((( #Z n) * f),x0)) = (( diff (( #Z n),(f . x0))) * ( diff (f,x0))) by A1, A2, FDIFF_2: 13

      .= ((n * ((f . x0) #Z (n - 1))) * ( diff (f,x0))) by Th2;

    end;

    

     Lm1: (( exp_R x) #R n) = ( exp_R (n * x))

    proof

      reconsider x as Real;

      defpred P[ Nat] means (( exp_R x) #R $1) = ( exp_R ($1 * x));

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A2: P[k];

        reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

        

        thus (( exp_R x) #R (k + 1)) = ((( exp_R x) #R k) * (( exp_R x) #R 1)) by PREPOWER: 75, SIN_COS: 55

        .= ((( exp_R x) #R k) * ( exp_R x)) by PREPOWER: 72, SIN_COS: 55

        .= ( exp_R ((k1 * x) + x)) by A2, SIN_COS: 50

        .= ( exp_R ((k + 1) * x));

      end;

      

       A3: P[ 0 ] by PREPOWER: 71, SIN_COS: 51, SIN_COS: 55;

      for n be Nat holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: TAYLOR_1:4

    

     Th4: ( exp_R ( - x)) = (1 / ( exp_R x))

    proof

      reconsider x as Real;

      (( exp_R ( - x)) * ( exp_R x)) = ( exp_R (( - x) + x)) by SIN_COS: 50

      .= 1 by SIN_COS: 51;

      hence thesis by XCMPLX_1: 73;

    end;

    

     Lm2: (( exp_R x) #R i) = ( exp_R (i * x))

    proof

      consider n be Nat such that

       A1: i = n or i = ( - n) by INT_1: 2;

      now

        per cases by A1;

          case i = n;

          hence thesis by Lm1;

        end;

          case

           A2: i = ( - n);

          

          hence ( exp_R (i * x)) = ( exp_R ( - (n * x)))

          .= (1 / ( exp_R (n * x))) by Th4

          .= (1 / (( exp_R x) #R n)) by Lm1

          .= (( exp_R x) #R i) by A2, PREPOWER: 76, SIN_COS: 55;

        end;

      end;

      hence thesis;

    end;

    theorem :: TAYLOR_1:5

    

     Th5: (( exp_R x) #R (1 / i)) = ( exp_R (x / i))

    proof

      set n = i;

      per cases ;

        suppose

         A1: n <> 0 ;

        

        then ( exp_R x) = ( exp_R ((x / n) * n)) by XCMPLX_1: 87

        .= (( exp_R (x / n)) #R n) by Lm2;

        

        hence (( exp_R x) #R (1 / n)) = (( exp_R (x / n)) #R (n * (1 / n))) by PREPOWER: 91, SIN_COS: 55

        .= (( exp_R (x / n)) #R 1) by A1, XCMPLX_1: 106

        .= ( exp_R (x / n)) by PREPOWER: 72, SIN_COS: 55;

      end;

        suppose

         A2: n = 0 ;

        (( exp_R x) #R (1 / 0 )) = ( exp_R 0 ) by PREPOWER: 71, SIN_COS: 51, SIN_COS: 55

        .= ( exp_R (x / 0 )) by XCMPLX_1: 49;

        hence thesis by A2;

      end;

    end;

    theorem :: TAYLOR_1:6

    

     Th6: for m,n be Integer holds (( exp_R x) #R (m / n)) = ( exp_R ((m / n) * x))

    proof

      let m,n be Integer;

      

      thus ( exp_R ((m / n) * x)) = ( exp_R ((x / n) * m)) by XCMPLX_1: 75

      .= (( exp_R (x / n)) #R m) by Lm2

      .= ((( exp_R x) #R (1 / n)) #R m) by Th5

      .= (( exp_R x) #R ((1 / n) * m)) by PREPOWER: 91, SIN_COS: 55

      .= (( exp_R x) #R ((m / n) * 1)) by XCMPLX_1: 75

      .= (( exp_R x) #R (m / n));

    end;

    

     Lm3: (( exp_R x) #R q) = ( exp_R (q * x))

    proof

      ex m be Integer, n be Nat st n <> 0 & q = (m / n) by RAT_1: 8;

      hence thesis by Th6;

    end;

    theorem :: TAYLOR_1:7

    

     Th7: (( exp_R x) #Q q) = ( exp_R (q * x))

    proof

      

      thus (( exp_R x) #Q q) = (( exp_R x) #R q) by PREPOWER: 74, SIN_COS: 55

      .= ( exp_R (q * x)) by Lm3;

    end;

    theorem :: TAYLOR_1:8

    

     Th8: (( exp_R x) #R p) = ( exp_R (p * x))

    proof

      ( exp_R x) > 0 by SIN_COS: 55;

      then

      consider s be Rational_Sequence such that

       A1: s is convergent & ( lim s) = p and (( exp_R x) #Q s) is convergent and

       A2: ( lim (( exp_R x) #Q s)) = (( exp_R x) #R p) by PREPOWER:def 7;

      

       A3: exp_R is_continuous_in (x * p) & ( rng (x (#) s)) c= ( dom exp_R ) by FDIFF_1: 24, SIN_COS: 47, SIN_COS: 65;

       A4:

      now

        let ii be object;

        assume ii in NAT ;

        then

        reconsider i = ii as Element of NAT ;

        

         A5: ( rng (x (#) s)) c= ( dom exp_R ) by SIN_COS: 47;

        

        thus ((( exp_R x) #Q s) . ii) = (( exp_R x) #Q (s . i)) by PREPOWER:def 6

        .= ( exp_R ((s . i) * x)) by Th7

        .= ( exp_R ((x (#) s) . i)) by SEQ_1: 9

        .= ( exp_R . ((x (#) s) . i)) by SIN_COS:def 23

        .= (( exp_R /* (x (#) s)) . ii) by A5, FUNCT_2: 108;

      end;

      (x (#) s) is convergent & ( lim (x (#) s)) = (x * p) by A1, SEQ_2: 7, SEQ_2: 8;

      

      then ( lim ( exp_R /* (x (#) s))) = ( exp_R . (x * p)) by A3, FCONT_1:def 1

      .= ( exp_R (p * x)) by SIN_COS:def 23;

      hence thesis by A2, A4, FUNCT_2: 12;

    end;

    theorem :: TAYLOR_1:9

    

     Th9: (( exp_R 1) #R x) = ( exp_R x) & (( exp_R 1) to_power x) = ( exp_R x) & ( number_e to_power x) = ( exp_R x) & ( number_e #R x) = ( exp_R x)

    proof

      

      thus

       A1: ( exp_R x) = ( exp_R (x * 1))

      .= (( exp_R 1) #R x) by Th8;

      ( exp_R 1) > 0 by SIN_COS: 55;

      hence thesis by A1, IRRAT_1:def 7, POWER:def 2;

    end;

    theorem :: TAYLOR_1:10

    (( exp_R . 1) #R x) = ( exp_R . x) & (( exp_R . 1) to_power x) = ( exp_R . x) & ( number_e to_power x) = ( exp_R . x) & ( number_e #R x) = ( exp_R . x)

    proof

      

      thus (( exp_R . 1) #R x) = (( exp_R 1) #R x) by SIN_COS:def 23

      .= ( exp_R x) by Th9

      .= ( exp_R . x) by SIN_COS:def 23;

      

      thus (( exp_R . 1) to_power x) = (( exp_R 1) to_power x) by SIN_COS:def 23

      .= ( exp_R x) by Th9

      .= ( exp_R . x) by SIN_COS:def 23;

      

      thus ( number_e to_power x) = ( exp_R x) by Th9

      .= ( exp_R . x) by SIN_COS:def 23;

      

      thus ( number_e #R x) = ( exp_R x) by Th9

      .= ( exp_R . x) by SIN_COS:def 23;

    end;

    theorem :: TAYLOR_1:11

     number_e > 2

    proof

      

       A1: number_e is irrational by IRRAT_1: 41;

      

       A5: for n be Element of NAT st 1 <= n holds (( Partial_Sums (1 rExpSeq )) . n) >= 2

      proof

        defpred X[ Integer] means (( Partial_Sums (1 rExpSeq )) . $1) >= 2;

        

         A6: for ni be Integer st 1 <= ni holds X[ni] implies X[(ni + 1)]

        proof

          let ni be Integer;

          assume 1 <= ni;

          then

          reconsider n = ni as Element of NAT by INT_1: 3;

          

           A7: (( Partial_Sums (1 rExpSeq )) . (n + 1)) = ((( Partial_Sums (1 rExpSeq )) . n) + ((1 rExpSeq ) . (n + 1))) by SERIES_1:def 1

          .= ((( Partial_Sums (1 rExpSeq )) . n) + ((1 |^ (n + 1)) / ((n + 1) ! ))) by SIN_COS:def 5;

          

           A8: ((( Partial_Sums (1 rExpSeq )) . n) + ((1 |^ (n + 1)) / ((n + 1) ! ))) > (( Partial_Sums (1 rExpSeq )) . n) by XREAL_1: 29, XREAL_1: 139;

          assume (( Partial_Sums (1 rExpSeq )) . ni) >= 2;

          hence thesis by A7, A8, XXREAL_0: 2;

        end;

        (( Partial_Sums (1 rExpSeq )) . 1) = ((( Partial_Sums (1 rExpSeq )) . 0 ) + ((1 rExpSeq ) . ( 0 + 1))) by SERIES_1:def 1

        .= (((1 rExpSeq ) . 0 ) + ((1 rExpSeq ) . 1)) by SERIES_1:def 1

        .= (((1 rExpSeq ) . 0 ) + ((1 |^ 1) / (1 ! ))) by SIN_COS:def 5

        .= (((1 |^ 0 ) / ( 0 ! )) + ((1 |^ 1) / (1 ! ))) by SIN_COS:def 5

        .= (1 + ((1 |^ 1) / (1 ! ))) by NEWTON: 12

        .= (1 + (1 / 1)) by NEWTON: 13

        .= 2;

        then

         A9: X[1];

        for n be Integer st 1 <= n holds X[n] from INT_1:sch 2( A9, A6);

        hence thesis;

      end;

      

       A10: for n be Nat holds ((( Partial_Sums (1 rExpSeq )) ^\ 1) . n) >= 2

      proof

        let n be Nat;

        ((( Partial_Sums (1 rExpSeq )) ^\ 1) . n) = (( Partial_Sums (1 rExpSeq )) . (n + 1)) by NAT_1:def 3;

        hence thesis by A5, NAT_1: 11;

      end;

      (1 rExpSeq ) is summable by SIN_COS: 45;

      then

       A11: ( Partial_Sums (1 rExpSeq )) is convergent by SERIES_1:def 2;

      ( lim ( Partial_Sums (1 rExpSeq ))) = ( Sum (1 rExpSeq )) by SERIES_1:def 3;

      then ( lim (( Partial_Sums (1 rExpSeq )) ^\ 1)) = ( Sum (1 rExpSeq )) by A11, SEQ_4: 20;

      then ( Sum (1 rExpSeq )) >= 2 by A10, A11, SIN_COS: 38;

      then ( exp_R . 1) >= 2 by SIN_COS:def 22;

      then number_e >= 2 by IRRAT_1:def 7, SIN_COS:def 23;

      then number_e > 2 or number_e = 2 by XXREAL_0: 1;

      hence thesis by A1;

    end;

    then

     Lm4: number_e > 1 by XXREAL_0: 2;

    registration

      cluster number_e -> positive;

      coherence by Lm4;

    end

    theorem :: TAYLOR_1:12

    

     Th12: ( log ( number_e ,( exp_R x))) = x

    proof

      ( exp_R x) > 0 & ( number_e to_power x) = ( exp_R x) by Th9, SIN_COS: 55;

      hence thesis by Lm4, POWER:def 3;

    end;

    theorem :: TAYLOR_1:13

    

     Th13: ( log ( number_e ,( exp_R . x))) = x

    proof

      

      thus ( log ( number_e ,( exp_R . x))) = ( log ( number_e ,( exp_R x))) by SIN_COS:def 23

      .= x by Th12;

    end;

    theorem :: TAYLOR_1:14

    

     Th14: y > 0 implies ( exp_R ( log ( number_e ,y))) = y

    proof

      assume y > 0 ;

      then ( number_e to_power ( log ( number_e ,y))) = y by Lm4, POWER:def 3;

      hence thesis by Th9;

    end;

    theorem :: TAYLOR_1:15

    

     Th15: y > 0 implies ( exp_R . ( log ( number_e ,y))) = y

    proof

      assume

       A1: y > 0 ;

      

      thus ( exp_R . ( log ( number_e ,y))) = ( exp_R ( log ( number_e ,y))) by SIN_COS:def 23

      .= y by A1, Th14;

    end;

    theorem :: TAYLOR_1:16

    

     Th16: exp_R is one-to-one & exp_R is_differentiable_on REAL & exp_R is_differentiable_on ( [#] REAL ) & (for x be Real holds ( diff ( exp_R ,x)) = ( exp_R . x)) & (for x be Real holds 0 < ( diff ( exp_R ,x))) & ( dom exp_R ) = ( [#] REAL ) & ( rng exp_R ) = ( right_open_halfline 0 )

    proof

      now

        let x1,x2 be object such that

         A1: x1 in ( dom exp_R ) and

         A2: x2 in ( dom exp_R ) and

         A3: ( exp_R . x1) = ( exp_R . x2);

        reconsider p2 = x2 as Real by A2;

        reconsider p1 = x1 as Real by A1;

        

        thus x1 = ( log ( number_e ,( exp_R . p1))) by Th13

        .= ( log ( number_e ,( exp_R . p2))) by A3

        .= x2 by Th13;

      end;

      hence exp_R is one-to-one by FUNCT_1:def 4;

      thus exp_R is_differentiable_on REAL & exp_R is_differentiable_on ( [#] REAL ) by SIN_COS: 66;

      thus for x be Real holds ( diff ( exp_R ,x)) = ( exp_R . x) by SIN_COS: 66;

      hereby

        let x be Real;

        ( diff ( exp_R ,x)) = ( exp_R . x) by SIN_COS: 66;

        hence ( diff ( exp_R ,x)) > 0 by SIN_COS: 54;

      end;

      thus ( dom exp_R ) = ( [#] REAL ) by SIN_COS: 47;

      now

        let y be object;

        assume y in ( rng exp_R );

        then

        consider x be object such that

         A4: x in ( dom exp_R ) and

         A5: y = ( exp_R . x) by FUNCT_1:def 3;

        reconsider y1 = y as Real by A5;

        reconsider x as Real by A4;

        ( exp_R . x) > 0 by SIN_COS: 54;

        then y1 in { g where g be Real : 0 < g } by A5;

        hence y in ( right_open_halfline 0 ) by XXREAL_1: 230;

      end;

      then

       A6: ( rng exp_R ) c= ( right_open_halfline 0 ) by TARSKI:def 3;

      now

        let y be object;

        assume y in ( right_open_halfline 0 );

        then y in { g where g be Real : 0 < g } by XXREAL_1: 230;

        then

         A7: ex g be Real st y = g & 0 < g;

        then

        reconsider y1 = y as Real;

        

         A8: ( log ( number_e ,y1)) in REAL by XREAL_0:def 1;

        y1 = ( exp_R . ( log ( number_e ,y1))) by A7, Th15;

        hence y in ( rng exp_R ) by FUNCT_1:def 3, SIN_COS: 47, A8;

      end;

      then ( right_open_halfline 0 ) c= ( rng exp_R ) by TARSKI:def 3;

      hence ( rng exp_R ) = ( right_open_halfline 0 ) by A6, XBOOLE_0:def 10;

    end;

    registration

      cluster exp_R -> one-to-one;

      coherence by Th16;

    end

    theorem :: TAYLOR_1:17

    

     Th17: ( exp_R " ) is_differentiable_on ( dom ( exp_R " )) & for x be Real st x in ( dom ( exp_R " )) holds ( diff (( exp_R " ),x)) = (1 / x)

    proof

      thus ( exp_R " ) is_differentiable_on ( dom ( exp_R " )) by Th16, FDIFF_2: 45;

      let x be Real such that

       A1: x in ( dom ( exp_R " ));

      

       A2: x in ( rng exp_R ) by A1, FUNCT_1: 33;

      ( diff ( exp_R ,(( exp_R " ) . x))) = ( exp_R . (( exp_R " ) . x)) by Th16

      .= x by A2, FUNCT_1: 35;

      hence thesis by A1, Th16, FDIFF_2: 45;

    end;

    registration

      cluster ( right_open_halfline 0 ) -> non empty;

      coherence

      proof

        1 in { g where g be Real : 0 < g };

        hence thesis by XXREAL_1: 230;

      end;

    end

    definition

      let a be Real;

      :: TAYLOR_1:def2

      func log_ a -> PartFunc of REAL , REAL means

      : Def2: ( dom it ) = ( right_open_halfline 0 ) & for d be Element of ( right_open_halfline 0 ) holds (it . d) = ( log (a,d));

      existence

      proof

        defpred X[ set] means $1 in ( right_open_halfline 0 );

        reconsider a as Real;

        deffunc U( Real) = ( In (( log (a,$1)), REAL ));

        consider f be PartFunc of REAL , REAL such that

         A1: for d be Element of REAL holds d in ( dom f) iff X[d] and

         A2: for d be Element of REAL st d in ( dom f) holds (f /. d) = U(d) from PARTFUN2:sch 2;

        take f;

        for x be object st x in ( right_open_halfline 0 ) holds x in ( dom f) by A1;

        then

         A3: ( right_open_halfline 0 ) c= ( dom f) by TARSKI:def 3;

        for x be object st x in ( dom f) holds x in ( right_open_halfline 0 ) by A1;

        then ( dom f) c= ( right_open_halfline 0 ) by TARSKI:def 3;

        hence

         A4: ( dom f) = ( right_open_halfline 0 ) by A3, XBOOLE_0:def 10;

        let d be Element of ( right_open_halfline 0 );

        (f /. d) = U(d) by A2, A4;

        hence thesis by A4, PARTFUN1:def 6;

      end;

      uniqueness

      proof

        let f1,f2 be PartFunc of REAL , REAL ;

        assume that

         A5: ( dom f1) = ( right_open_halfline 0 ) and

         A6: for d be Element of ( right_open_halfline 0 ) holds (f1 . d) = ( log (a,d)) and

         A7: ( dom f2) = ( right_open_halfline 0 ) and

         A8: for d be Element of ( right_open_halfline 0 ) holds (f2 . d) = ( log (a,d));

        for d be Element of REAL st d in ( right_open_halfline 0 ) holds (f1 . d) = (f2 . d)

        proof

          let d be Element of REAL such that

           A9: d in ( right_open_halfline 0 );

          

          thus (f1 . d) = ( log (a,d)) by A6, A9

          .= (f2 . d) by A8, A9;

        end;

        hence f1 = f2 by A5, A7, PARTFUN1: 5;

      end;

    end

    definition

      :: TAYLOR_1:def3

      func ln -> PartFunc of REAL , REAL equals ( log_ number_e );

      correctness ;

    end

    theorem :: TAYLOR_1:18

    

     Th18: ln = ( exp_R " ) & ln is one-to-one & ( dom ln ) = ( right_open_halfline 0 ) & ( rng ln ) = REAL & ln is_differentiable_on ( right_open_halfline 0 ) & (for x be Real st x > 0 holds ln is_differentiable_in x) & (for x be Element of ( right_open_halfline 0 ) holds ( diff ( ln ,x)) = (1 / x)) & for x be Element of ( right_open_halfline 0 ) holds 0 < ( diff ( ln ,x))

    proof

      

       A1: for d be Element of REAL st d in ( right_open_halfline 0 ) holds (( exp_R " ) . d) = ( ln . d)

      proof

        let d be Element of REAL such that

         A2: d in ( right_open_halfline 0 );

        (( exp_R " ) . d) = ( log ( number_e ,d))

        proof

          

           A3: ( log ( number_e ,d)) in REAL by XREAL_0:def 1;

          d in { g where g be Real : 0 < g } by A2, XXREAL_1: 230;

          then ex g be Real st g = d & g > 0 ;

          then d = ( exp_R . ( log ( number_e ,d))) by Th15;

          hence thesis by Th16, FUNCT_1: 32, A3;

        end;

        hence thesis by A2, Def2;

      end;

      

       A4: ( dom ( exp_R " )) = ( right_open_halfline 0 ) by Th16, FUNCT_1: 33;

      then ( dom ( exp_R " )) = ( dom ln ) by Def2;

      hence

       A5: ln = ( exp_R " ) by A4, A1, PARTFUN1: 5;

      

       A6: for x be Real st x > 0 holds ln is_differentiable_in x

      proof

        let x be Real;

        assume x > 0 ;

        then x in { g where g be Real : 0 < g };

        then x in ( right_open_halfline 0 ) by XXREAL_1: 230;

        hence thesis by A4, A5, Th17, FDIFF_1: 9;

      end;

      

       A7: for x be Element of ( right_open_halfline 0 ) holds 0 < ( diff ( ln ,x))

      proof

        let x be Element of ( right_open_halfline 0 );

        x in ( right_open_halfline 0 );

        then x in { g where g be Real : 0 < g } by XXREAL_1: 230;

        then

         A8: ex g be Real st x = g & 0 < g;

        (1 / x) = (x " ) by XCMPLX_1: 215;

        hence thesis by A4, A5, A8, Th17;

      end;

      thus ln is one-to-one by A5, FUNCT_1: 40;

      ( dom ln ) = ( right_open_halfline 0 ) by Def2;

      hence thesis by A5, A6, A7, Th16, Th17, FUNCT_1: 33;

    end;

    theorem :: TAYLOR_1:19

    f is_differentiable_in x0 implies ( exp_R * f) is_differentiable_in x0 & ( diff (( exp_R * f),x0)) = (( exp_R . (f . x0)) * ( diff (f,x0)))

    proof

      assume

       A1: f is_differentiable_in x0;

      

       A2: x0 is Real & exp_R is_differentiable_in (f . x0) by Th16, FDIFF_1: 9, XREAL_0:def 1;

      hence ( exp_R * f) is_differentiable_in x0 by A1, FDIFF_2: 13;

      

      thus ( diff (( exp_R * f),x0)) = (( diff ( exp_R ,(f . x0))) * ( diff (f,x0))) by A1, A2, FDIFF_2: 13

      .= (( exp_R . (f . x0)) * ( diff (f,x0))) by Th16;

    end;

    theorem :: TAYLOR_1:20

    f is_differentiable_in x0 & (f . x0) > 0 implies ( ln * f) is_differentiable_in x0 & ( diff (( ln * f),x0)) = (( diff (f,x0)) / (f . x0))

    proof

      assume that

       A1: f is_differentiable_in x0 and

       A2: (f . x0) > 0 ;

      (f . x0) in { g where g be Real : 0 < g } by A2;

      then

       A3: (f . x0) in ( right_open_halfline 0 ) by XXREAL_1: 230;

      then

       A4: ln is_differentiable_in (f . x0) by Th18, FDIFF_1: 9;

      thus ( ln * f) is_differentiable_in x0 by A1, A4, FDIFF_2: 13;

      

      thus ( diff (( ln * f),x0)) = (( diff ( ln ,(f . x0))) * ( diff (f,x0))) by A1, A4, FDIFF_2: 13

      .= ((1 / (f . x0)) * ( diff (f,x0))) by A3, Th18

      .= ((( diff (f,x0)) / (f . x0)) * 1) by XCMPLX_1: 75

      .= (( diff (f,x0)) / (f . x0));

    end;

    definition

      let p be Real;

      :: TAYLOR_1:def4

      func #R p -> PartFunc of REAL , REAL means

      : Def4: ( dom it ) = ( right_open_halfline 0 ) & for d be Element of ( right_open_halfline 0 ) holds (it . d) = (d #R p);

      existence

      proof

        defpred X[ set] means $1 in ( right_open_halfline 0 );

        reconsider p as Real;

        deffunc U( Real) = ( In (($1 #R p), REAL ));

        consider f be PartFunc of REAL , REAL such that

         A1: for d be Element of REAL holds d in ( dom f) iff X[d] and

         A2: for d be Element of REAL st d in ( dom f) holds (f /. d) = U(d) from PARTFUN2:sch 2;

        take f;

        for x be object st x in ( right_open_halfline 0 ) holds x in ( dom f) by A1;

        then

         A3: ( right_open_halfline 0 ) c= ( dom f) by TARSKI:def 3;

        for x be object st x in ( dom f) holds x in ( right_open_halfline 0 ) by A1;

        then ( dom f) c= ( right_open_halfline 0 ) by TARSKI:def 3;

        hence

         A4: ( dom f) = ( right_open_halfline 0 ) by A3, XBOOLE_0:def 10;

        let d be Element of ( right_open_halfline 0 );

        (f /. d) = U(d) by A2, A4;

        hence thesis by A4, PARTFUN1:def 6;

      end;

      uniqueness

      proof

        let f1,f2 be PartFunc of REAL , REAL ;

        assume that

         A5: ( dom f1) = ( right_open_halfline 0 ) and

         A6: for d be Element of ( right_open_halfline 0 ) holds (f1 . d) = (d #R p) and

         A7: ( dom f2) = ( right_open_halfline 0 ) and

         A8: for d be Element of ( right_open_halfline 0 ) holds (f2 . d) = (d #R p);

        for d be Element of REAL st d in ( right_open_halfline 0 ) holds (f1 . d) = (f2 . d)

        proof

          let d be Element of REAL such that

           A9: d in ( right_open_halfline 0 );

          

          thus (f1 . d) = (d #R p) by A6, A9

          .= (f2 . d) by A8, A9;

        end;

        hence f1 = f2 by A5, A7, PARTFUN1: 5;

      end;

    end

    theorem :: TAYLOR_1:21

    

     Th21: x > 0 implies ( #R p) is_differentiable_in x & ( diff (( #R p),x)) = (p * (x #R (p - 1)))

    proof

      set f = ( #R p);

      

       A1: for x be Real st 0 < x holds ( exp_R * (p (#) ln )) is_differentiable_in x & ( diff (( exp_R * (p (#) ln )),x)) = (p * (x #R (p - 1)))

      proof

        let x be Real such that

         A2: x > 0 ;

        

         A3: ln is_differentiable_in x by A2, Th18;

        then

         A4: (p (#) ln ) is_differentiable_in x by FDIFF_1: 15;

        x in { g where g be Real : 0 < g } by A2;

        then

         A5: x in ( right_open_halfline 0 ) by XXREAL_1: 230;

        then

         A6: x in ( dom (p (#) ln )) by Th18, VALUED_1:def 5;

        

         A7: ( diff ((p (#) ln ),x)) = (p * ( diff ( ln ,x))) by A3, FDIFF_1: 15

        .= (p * (1 / x)) by A5, Th18;

        

         A8: exp_R is_differentiable_in ((p (#) ln ) . x) by SIN_COS: 65;

        hence ( exp_R * (p (#) ln )) is_differentiable_in x by A4, FDIFF_2: 13;

        ( diff ( exp_R ,((p (#) ln ) . x))) = ( exp_R . ((p (#) ln ) . x)) by Th16

        .= ( exp_R . (p * ( ln . x))) by A6, VALUED_1:def 5

        .= ( exp_R . (p * ( log ( number_e ,x)))) by A5, Def2

        .= ( exp_R . ( log ( number_e ,(x to_power p)))) by A2, Lm4, POWER: 55

        .= (x to_power p) by A2, Th15, POWER: 34;

        

        hence ( diff (( exp_R * (p (#) ln )),x)) = ((x to_power p) * (p * (1 / x))) by A4, A8, A7, FDIFF_2: 13

        .= (p * ((x to_power p) * (1 / x)))

        .= (p * ((x to_power p) * (1 / (x to_power 1)))) by POWER: 25

        .= (p * ((x to_power p) * (x to_power ( - 1)))) by A2, POWER: 28

        .= (p * (x to_power (p + ( - 1)))) by A2, POWER: 27

        .= (p * (x #R (p - 1))) by A2, POWER:def 2;

      end;

      ( rng (p (#) ln )) c= ( dom exp_R ) by Th16;

      

      then

       A9: ( dom ( exp_R * (p (#) ln ))) = ( dom (p (#) ln )) by RELAT_1: 27

      .= ( right_open_halfline 0 ) by Th18, VALUED_1:def 5;

      

       A10: for d be Element of REAL st d in ( right_open_halfline 0 ) holds (( exp_R * (p (#) ln )) . d) = (f . d)

      proof

        let d be Element of REAL such that

         A11: d in ( right_open_halfline 0 );

        

         A12: d in ( dom (p (#) ln )) by A11, Th18, VALUED_1:def 5;

        d in { g where g be Real : 0 < g } by A11, XXREAL_1: 230;

        then

         A13: ex g be Real st g = d & g > 0 ;

        

        thus (( exp_R * (p (#) ln )) . d) = (( exp_R * (p (#) ln )) /. d) by A9, A11, PARTFUN1:def 6

        .= ( exp_R /. ((p (#) ln ) /. d)) by A9, A11, PARTFUN2: 3

        .= ( exp_R . ((p (#) ln ) . d)) by A12, PARTFUN1:def 6

        .= ( exp_R . (p * ( ln . d))) by A12, VALUED_1:def 5

        .= ( exp_R . (p * ( log ( number_e ,d)))) by A11, Def2

        .= ( exp_R . ( log ( number_e ,(d to_power p)))) by A13, Lm4, POWER: 55

        .= (d to_power p) by A13, Th15, POWER: 34

        .= (d #R p) by A13, POWER:def 2

        .= (f . d) by A11, Def4;

      end;

      ( dom f) = ( right_open_halfline 0 ) by Def4;

      then x is Real & ( exp_R * (p (#) ln )) = f by A9, A10, PARTFUN1: 5;

      hence thesis by A1;

    end;

    theorem :: TAYLOR_1:22

    f is_differentiable_in x0 & (f . x0) > 0 implies (( #R p) * f) is_differentiable_in x0 & ( diff ((( #R p) * f),x0)) = ((p * ((f . x0) #R (p - 1))) * ( diff (f,x0)))

    proof

      assume that

       A1: f is_differentiable_in x0 and

       A2: (f . x0) > 0 ;

      

       A3: ( #R p) is_differentiable_in (f . x0) by A2, Th21;

      hence (( #R p) * f) is_differentiable_in x0 by A1, FDIFF_2: 13;

      

      thus ( diff ((( #R p) * f),x0)) = (( diff (( #R p),(f . x0))) * ( diff (f,x0))) by A1, A3, FDIFF_2: 13

      .= ((p * ((f . x0) #R (p - 1))) * ( diff (f,x0))) by A2, Th21;

    end;

    begin

    definition

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL ;

      :: TAYLOR_1:def5

      func diff (f,Z) -> Functional_Sequence of REAL , REAL means

      : Def5: (it . 0 ) = (f | Z) & for i be Nat holds (it . (i + 1)) = ((it . i) `| Z);

      existence

      proof

        reconsider fZ = (f | Z) as Element of ( PFuncs ( REAL , REAL )) by PARTFUN1: 45;

        defpred R[ set, set, set] means ex h be PartFunc of REAL , REAL st $2 = h & $3 = (h `| Z);

        

         A1: for n be Nat holds for x be Element of ( PFuncs ( REAL , REAL )) holds ex y be Element of ( PFuncs ( REAL , REAL )) st R[n, x, y]

        proof

          let n be Nat;

          let x be Element of ( PFuncs ( REAL , REAL ));

          reconsider x9 = x as PartFunc of REAL , REAL by PARTFUN1: 46;

          reconsider y = (x9 `| Z) as Element of ( PFuncs ( REAL , REAL )) by PARTFUN1: 45;

          ex h be PartFunc of REAL , REAL st x = h & y = (h `| Z);

          hence thesis;

        end;

        consider g be sequence of ( PFuncs ( REAL , REAL )) such that

         A2: (g . 0 ) = fZ & for n be Nat holds R[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 2( A1);

        reconsider g as Functional_Sequence of REAL , REAL ;

        take g;

        thus (g . 0 ) = (f | Z) by A2;

        let i be Nat;

         R[i, (g . i), (g . (i + 1))] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1,seq2 be Functional_Sequence of REAL , REAL ;

        assume that

         A3: (seq1 . 0 ) = (f | Z) and

         A4: for n be Nat holds (seq1 . (n + 1)) = ((seq1 . n) `| Z) and

         A5: (seq2 . 0 ) = (f | Z) and

         A6: for n be Nat holds (seq2 . (n + 1)) = ((seq2 . n) `| Z);

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);

        

         A7: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A8: P[k];

          

          thus (seq1 . (k + 1)) = ((seq1 . k) `| Z) by A4

          .= (seq2 . (k + 1)) by A6, A8;

        end;

        

         A9: P[ 0 ] by A3, A5;

        for n be Nat holds P[n] from NAT_1:sch 2( A9, A7);

        hence seq1 = seq2;

      end;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      let n be Nat;

      let Z be Subset of REAL ;

      :: TAYLOR_1:def6

      pred f is_differentiable_on n,Z means for i be Nat st i <= (n - 1) holds (( diff (f,Z)) . i) is_differentiable_on Z;

    end

    theorem :: TAYLOR_1:23

    

     Th23: for f be PartFunc of REAL , REAL , Z be Subset of REAL , n be Nat st f is_differentiable_on (n,Z) holds for m be Nat st m <= n holds f is_differentiable_on (m,Z)

    proof

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL ;

      let n be Nat such that

       A1: f is_differentiable_on (n,Z);

      let m be Nat such that

       A2: m <= n;

      now

        

         A3: (m - 1) <= (n - 1) by A2, XREAL_1: 13;

        let i be Nat;

        assume i <= (m - 1);

        then i <= (n - 1) by A3, XXREAL_0: 2;

        hence (( diff (f,Z)) . i) is_differentiable_on Z by A1;

      end;

      hence thesis;

    end;

    definition

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL ;

      let a,b be Real;

      :: TAYLOR_1:def7

      func Taylor (f,Z,a,b) -> Real_Sequence means

      : Def7: for n be Nat holds (it . n) = ((((( diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n ! ));

      existence

      proof

        deffunc F( Nat) = ((((( diff (f,Z)) . $1) . a) * ((b - a) |^ $1)) / ($1 ! ));

        consider seq be Real_Sequence such that

         A1: for n be Nat holds (seq . n) = F(n) from SEQ_1:sch 1;

        take seq;

        let n be Nat;

        thus thesis by A1;

      end;

      uniqueness

      proof

        deffunc F( Nat) = ((((( diff (f,Z)) . $1) . a) * ((b - a) |^ $1)) / ($1 ! ));

        let s1,s2 be Real_Sequence such that

         A2: for n be Nat holds (s1 . n) = F(n) and

         A3: for n be Nat holds (s2 . n) = F(n);

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider n = x as Element of NAT ;

          

          thus (s1 . x) = F(n) by A2

          .= (s2 . x) by A3;

        end;

        hence thesis;

      end;

    end

    

     Lm5: for b be Real holds ex g be PartFunc of REAL , REAL st (( dom g) = ( [#] REAL ) & for x be Real holds (g . x) = (b - x) & for x be Real holds g is_differentiable_in x & ( diff (g,x)) = ( - 1))

    proof

      defpred X[ set] means $1 in REAL ;

      let b be Real;

      deffunc U( Real) = ( In ((b - $1), REAL ));

      consider g be PartFunc of REAL , REAL such that

       A1: for d be Element of REAL holds d in ( dom g) iff X[d] and

       A2: for d be Element of REAL st d in ( dom g) holds (g /. d) = U(d) from PARTFUN2:sch 2;

      take g;

      for x be object st x in REAL holds x in ( dom g) by A1;

      then

       A3: REAL c= ( dom g) by TARSKI:def 3;

      then

       A4: ( dom g) = ( [#] REAL ) by XBOOLE_0:def 10;

      

       A5: for d be Real holds (g . d) = (b - d)

      proof

        let d be Real;

        reconsider d as Element of REAL by XREAL_0:def 1;

        (g /. d) = U(d) by A2, A4;

        hence thesis by A4, PARTFUN1:def 6;

      end;

      

       A6: for d be Real st d in REAL holds (g . d) = ((( - 1) * d) + b)

      proof

        let d be Real;

        assume d in REAL ;

        

        thus (g . d) = (b - d) by A5

        .= ((( - 1) * d) + b);

      end;

      then

       A7: g is_differentiable_on ( dom g) by A4, FDIFF_1: 23;

      for x be Real holds g is_differentiable_in x & ( diff (g,x)) = ( - 1)

      proof

        let dd be Real;

        reconsider d = dd as Element of REAL by XREAL_0:def 1;

        g is_differentiable_in d by A4, A7, FDIFF_1: 9;

        hence g is_differentiable_in dd;

        

        thus ( diff (g,dd)) = ((g `| ( dom g)) . d) by A4, A7, FDIFF_1:def 7

        .= ( - 1) by A4, A6, FDIFF_1: 23;

      end;

      hence thesis by A3, A5, XBOOLE_0:def 10;

    end;

    

     Lm6: for n be Nat holds for l,b be Real holds ex g be PartFunc of REAL , REAL st ( dom g) = ( [#] REAL ) & (for x be Real holds (g . x) = ((l * ((b - x) |^ (n + 1))) / ((n + 1) ! ))) & for x be Real holds g is_differentiable_in x & ( diff (g,x)) = ( - ((l * ((b - x) |^ n)) / (n ! )))

    proof

      defpred X[ set] means $1 in REAL ;

      let n be Nat;

      let l,b be Real;

      deffunc U( Real) = ( In (((l * ((b - $1) |^ (n + 1))) / ((n + 1) ! )), REAL ));

      consider g be PartFunc of REAL , REAL such that

       A1: for d be Element of REAL holds d in ( dom g) iff X[d] and

       A2: for d be Element of REAL st d in ( dom g) holds (g /. d) = U(d) from PARTFUN2:sch 2;

      take g;

      consider f be PartFunc of REAL , REAL such that

       A3: ( dom f) = ( [#] REAL ) and

       A4: for x be Real holds (f . x) = (b - x) and

       A5: for x be Real holds f is_differentiable_in x & ( diff (f,x)) = ( - 1) by Lm5;

      ( dom ( #Z (n + 1))) = REAL & ( rng f) c= REAL by FUNCT_2:def 1;

      then

       A6: ( dom (( #Z (n + 1)) * f)) = ( dom f) by RELAT_1: 27;

      for x be object st x in REAL holds x in ( dom g) by A1;

      then

       A7: REAL c= ( dom g) by TARSKI:def 3;

      then

       A8: ( dom g) = ( [#] REAL ) by XBOOLE_0:def 10;

      

       A9: for d be Real holds (g . d) = ((l * ((b - d) |^ (n + 1))) / ((n + 1) ! ))

      proof

        let d be Real;

        reconsider d as Element of REAL by XREAL_0:def 1;

        (g /. d) = U(d) by A2, A8;

        hence thesis by A8, PARTFUN1:def 6;

      end;

       A10:

      now

        let x be Element of REAL ;

        assume x in ( dom ((l / ((n + 1) ! )) (#) (( #Z (n + 1)) * f)));

        

        hence (((l / ((n + 1) ! )) (#) (( #Z (n + 1)) * f)) . x) = ((l / ((n + 1) ! )) * ((( #Z (n + 1)) * f) . x)) by VALUED_1:def 5

        .= ((l / ((n + 1) ! )) * ((( #Z (n + 1)) * f) /. x)) by A3, A6, PARTFUN1:def 6

        .= ((l / ((n + 1) ! )) * (( #Z (n + 1)) /. (f /. x))) by A3, A6, PARTFUN2: 3

        .= ((l / ((n + 1) ! )) * (( #Z (n + 1)) . (f . x))) by A3, PARTFUN1:def 6

        .= ((l / ((n + 1) ! )) * ((f . x) #Z (n + 1))) by Def1

        .= ((l / ((n + 1) ! )) * ((f . x) |^ (n + 1))) by PREPOWER: 36

        .= ((l / ((n + 1) ! )) * ((b - x) |^ (n + 1))) by A4

        .= ((l * ((b - x) |^ (n + 1))) / ((n + 1) ! )) by XCMPLX_1: 74

        .= (g . x) by A9;

      end;

      

       A11: for x be Real holds (( #Z (n + 1)) * f) is_differentiable_in x & ( diff ((( #Z (n + 1)) * f),x)) = ( - ((n + 1) * ((b - x) #Z n)))

      proof

        let xx be Real;

        reconsider x = xx as Real;

        

         A12: f is_differentiable_in x & ( #Z (n + 1)) is_differentiable_in (f . x) by A5, Th2;

        hence (( #Z (n + 1)) * f) is_differentiable_in xx by FDIFF_2: 13;

        ( diff (( #Z (n + 1)),(f . x))) = ((n + 1) * ((f . x) #Z ((n + 1) - 1))) by Th2;

        

        hence ( diff ((( #Z (n + 1)) * f),xx)) = (((n + 1) * ((f . x) #Z ((n + 1) - 1))) * ( diff (f,x))) by A12, FDIFF_2: 13

        .= (((n + 1) * ((f . x) #Z ((n + 1) - 1))) * ( - 1)) by A5

        .= (((n + 1) * ((b - x) #Z ((n + 1) - 1))) * ( - 1)) by A4

        .= ( - ((n + 1) * ((b - xx) #Z n)));

      end;

       A13:

      now

        let x be Real;

        

         A14: ((n + 1) / ((n + 1) ! )) = ((1 * (n + 1)) / ((n ! ) * (n + 1))) by NEWTON: 15

        .= (1 / (n ! )) by XCMPLX_1: 91;

        

         A15: (( #Z (n + 1)) * f) is_differentiable_in x by A11;

        hence ((l / ((n + 1) ! )) (#) (( #Z (n + 1)) * f)) is_differentiable_in x by FDIFF_1: 15;

        

        thus ( diff (((l / ((n + 1) ! )) (#) (( #Z (n + 1)) * f)),x)) = ((l / ((n + 1) ! )) * ( diff ((( #Z (n + 1)) * f),x))) by A15, FDIFF_1: 15

        .= ((( diff ((( #Z (n + 1)) * f),x)) / ((n + 1) ! )) * l) by XCMPLX_1: 75

        .= (l * (( - ((n + 1) * ((b - x) #Z n))) / ((n + 1) ! ))) by A11

        .= (l * (( - ((n + 1) * ((b - x) |^ n))) / ((n + 1) ! ))) by PREPOWER: 36

        .= ((l * ( - ((n + 1) * ((b - x) |^ n)))) / ((n + 1) ! )) by XCMPLX_1: 74

        .= ((( - l) * ((n + 1) * ((b - x) |^ n))) / ((n + 1) ! ))

        .= (( - l) * (((n + 1) * ((b - x) |^ n)) / ((n + 1) ! ))) by XCMPLX_1: 74

        .= (( - l) * (((b - x) |^ n) * ((n + 1) / ((n + 1) ! )))) by XCMPLX_1: 74

        .= (( - l) * (((b - x) |^ n) / (n ! ))) by A14, XCMPLX_1: 99

        .= ( - (l * (((b - x) |^ n) / (n ! ))))

        .= ( - ((l * ((b - x) |^ n)) / (n ! ))) by XCMPLX_1: 74;

      end;

      ( dom ((l / ((n + 1) ! )) (#) (( #Z (n + 1)) * f))) = ( dom g) by A8, A3, A6, VALUED_1:def 5;

      then ((l / ((n + 1) ! )) (#) (( #Z (n + 1)) * f)) = g by A10, PARTFUN1: 5;

      hence thesis by A7, A9, A13, XBOOLE_0:def 10;

    end;

    

     Lm7: for n be Nat holds for f be PartFunc of REAL , REAL holds for Z be Subset of REAL holds for b be Real holds ex g be PartFunc of REAL , REAL st (( dom g) = Z & for x be Real st x in Z holds (g . x) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . n)))

    proof

      let n be Nat;

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL ;

      let b be Real;

      defpred X[ set] means $1 in Z;

      deffunc U( Real) = ( In (((f . b) - (( Partial_Sums ( Taylor (f,Z,$1,b))) . n)), REAL ));

      consider g be PartFunc of REAL , REAL such that

       A1: for d be Element of REAL holds d in ( dom g) iff X[d] and

       A2: for d be Element of REAL st d in ( dom g) holds (g /. d) = U(d) from PARTFUN2:sch 2;

      take g;

      for x be object st x in ( dom g) holds x in Z by A1;

      then

       A3: ( dom g) c= Z by TARSKI:def 3;

      for x be object st x in Z holds x in ( dom g) by A1;

      then

       A4: Z c= ( dom g) by TARSKI:def 3;

      for d be Real st d in Z holds (g . d) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,d,b))) . n))

      proof

        let d be Real such that

         A5: d in Z;

        (g /. d) = U(d) by A2, A4, A5

        .= ((f . b) - (( Partial_Sums ( Taylor (f,Z,d,b))) . n));

        hence thesis by A4, A5, PARTFUN1:def 6;

      end;

      hence thesis by A3, A4, XBOOLE_0:def 10;

    end;

    theorem :: TAYLOR_1:24

    

     Th24: for f be PartFunc of REAL , REAL , Z be Subset of REAL , n be Nat st f is_differentiable_on (n,Z) holds for a,b be Real st a < b & ].a, b.[ c= Z holds ((( diff (f,Z)) . n) | ].a, b.[) = (( diff (f, ].a, b.[)) . n)

    proof

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL ;

      defpred P[ Nat] means f is_differentiable_on ($1,Z) implies for a,b be Real st a < b & ].a, b.[ c= Z holds ((( diff (f,Z)) . $1) | ].a, b.[) = (( diff (f, ].a, b.[)) . $1);

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A2: P[k];

        assume

         A3: f is_differentiable_on ((k + 1),Z);

        let a,b be Real such that

         A4: a < b and

         A5: ].a, b.[ c= Z;

        

         A6: (( diff (f,Z)) . k) is_differentiable_on Z by A3;

        then

         A7: (( diff (f,Z)) . k) is_differentiable_on ].a, b.[ by A5, FDIFF_1: 26;

        then

         A8: ( dom ((( diff (f,Z)) . k) `| ].a, b.[)) = ].a, b.[ by FDIFF_1:def 7;

        

         A9: ( dom (((( diff (f,Z)) . k) `| Z) | ].a, b.[)) = (( dom ((( diff (f,Z)) . k) `| Z)) /\ ].a, b.[) by RELAT_1: 61

        .= (Z /\ ].a, b.[) by A6, FDIFF_1:def 7

        .= ].a, b.[ by A5, XBOOLE_1: 28;

         A10:

        now

          let x be Element of REAL such that

           A11: x in ( dom (((( diff (f,Z)) . k) `| Z) | ].a, b.[));

          

          thus ((((( diff (f,Z)) . k) `| Z) | ].a, b.[) . x) = (((( diff (f,Z)) . k) `| Z) . x) by A9, A11, FUNCT_1: 49

          .= ( diff ((( diff (f,Z)) . k),x)) by A5, A6, A9, A11, FDIFF_1:def 7

          .= (((( diff (f,Z)) . k) `| ].a, b.[) . x) by A7, A9, A11, FDIFF_1:def 7;

        end;

        

        thus ((( diff (f,Z)) . (k + 1)) | ].a, b.[) = (((( diff (f,Z)) . k) `| Z) | ].a, b.[) by Def5

        .= ((( diff (f,Z)) . k) `| ].a, b.[) by A9, A8, A10, PARTFUN1: 5

        .= (((( diff (f,Z)) . k) | ].a, b.[) `| ].a, b.[) by A7, FDIFF_2: 16

        .= ((( diff (f, ].a, b.[)) . k) `| ].a, b.[) by A2, A3, A4, A5, Th23, NAT_1: 11

        .= (( diff (f, ].a, b.[)) . (k + 1)) by Def5;

      end;

      

       A12: P[ 0 ]

      proof

        assume f is_differentiable_on ( 0 ,Z);

        let a,b be Real such that a < b and

         A13: ].a, b.[ c= Z;

        

        thus ((( diff (f,Z)) . 0 ) | ].a, b.[) = ((f | Z) | ].a, b.[) by Def5

        .= (f | ].a, b.[) by A13, FUNCT_1: 51

        .= (( diff (f, ].a, b.[)) . 0 ) by Def5;

      end;

      thus for k be Nat holds P[k] from NAT_1:sch 2( A12, A1);

    end;

    

     Lm8: for f be PartFunc of REAL , REAL , Z be Subset of REAL st Z c= ( dom f) holds for n be Nat st f is_differentiable_on (n,Z) holds for a,b be Real st a < b & [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[) holds for g be PartFunc of REAL , REAL st ( dom g) = Z & for x be Real st x in Z holds (g . x) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . n)) holds (g . b) = 0 & (g | [.a, b.]) is continuous & g is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (g,x)) = ( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! )))

    proof

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL such that

       A1: Z c= ( dom f);

      defpred P[ Nat] means f is_differentiable_on ($1,Z) implies for a,b be Real st a < b & [.a, b.] c= Z & ((( diff (f,Z)) . $1) | [.a, b.]) is continuous & f is_differentiable_on (($1 + 1), ].a, b.[) holds for g be PartFunc of REAL , REAL st ( dom g) = Z & for x be Real st x in Z holds (g . x) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . $1)) holds (g . b) = 0 & (g | [.a, b.]) is continuous & g is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (g,x)) = ( - ((((( diff (f, ].a, b.[)) . ($1 + 1)) . x) * ((b - x) |^ $1)) / ($1 ! )));

      

       A2: P[ 0 ]

      proof

        assume f is_differentiable_on ( 0 ,Z);

        let a,b be Real such that

         A3: a < b and

         A4: [.a, b.] c= Z and

         A5: ((( diff (f,Z)) . 0 ) | [.a, b.]) is continuous and

         A6: f is_differentiable_on (( 0 + 1), ].a, b.[);

        

         A7: ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

        then

         A8: ].a, b.[ c= Z by A4, XBOOLE_1: 1;

        let g be PartFunc of REAL , REAL such that

         A9: ( dom g) = Z and

         A10: for x be Real st x in Z holds (g . x) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . 0 ));

        

         A11: b in [.a, b.] by A3, XXREAL_1: 1;

        

        hence (g . b) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,b,b))) . 0 )) by A4, A10

        .= ((f . b) - (( Taylor (f,Z,b,b)) . 0 )) by SERIES_1:def 1

        .= ((f . b) - ((((( diff (f,Z)) . 0 ) . b) * ((b - b) |^ 0 )) / ( 0 ! ))) by Def7

        .= ((f . b) - ((((f | Z) . b) * ((b - b) |^ 0 )) / ( 0 ! ))) by Def5

        .= ((f . b) - (((f . b) * ((b - b) |^ 0 )) / ( 0 ! ))) by A4, A11, FUNCT_1: 49

        .= ((f . b) - ((f . b) * 1)) by NEWTON: 4, NEWTON: 12

        .= 0 ;

        consider y be PartFunc of REAL , REAL such that

         A12: ( dom y) = ( [#] REAL ) and

         A13: for x be Real holds (y . x) = ((f . b) - x) and

         A14: for x be Real holds y is_differentiable_in x & ( diff (y,x)) = ( - 1) by Lm5;

        ( rng f) c= REAL ;

        then

         A15: ( dom (y * f)) = ( dom f) by A12, RELAT_1: 27;

        for x be Real st x in REAL holds y is_differentiable_in x by A14;

        then y is_differentiable_on REAL by A12, FDIFF_1: 9;

        then (y | REAL ) is continuous by FDIFF_1: 25;

        then

         A16: (y | (f .: [.a, b.])) is continuous by FCONT_1: 16;

        ( rng f) c= ( dom y) by A12;

        then

         A17: ( dom (y * f)) = ( dom f) by RELAT_1: 27;

        

         A18: [.a, b.] c= ( dom f) by A1, A4, XBOOLE_1: 1;

        then

         A19: ].a, b.[ c= ( dom f) by A7, XBOOLE_1: 1;

        (( diff (f, ].a, b.[)) . 0 ) is_differentiable_on ].a, b.[ by A6;

        then (f | ].a, b.[) is_differentiable_on ].a, b.[ by Def5;

        then for x be Real st x in ].a, b.[ holds (f | ].a, b.[) is_differentiable_in x by FDIFF_1: 9;

        then

         A20: f is_differentiable_on ].a, b.[ by A19, FDIFF_1:def 6;

        

         A21: for x be Real st x in ].a, b.[ holds (y * f) is_differentiable_in x & ( diff ((y * f),x)) = ( - ((((( diff (f, ].a, b.[)) . ( 0 + 1)) . x) * ((b - x) |^ 0 )) / ( 0 ! )))

        proof

          

           A22: (( diff (f, ].a, b.[)) . ( 0 + 1)) = ((( diff (f, ].a, b.[)) . 0 ) `| ].a, b.[) by Def5

          .= ((f | ].a, b.[) `| ].a, b.[) by Def5

          .= (f `| ].a, b.[) by A20, FDIFF_2: 16;

          let x be Real such that

           A23: x in ].a, b.[;

          

           A24: f is_differentiable_in x by A20, A23, FDIFF_1: 9;

          

           A25: y is_differentiable_in (f . x) by A14;

          hence (y * f) is_differentiable_in x by A24, FDIFF_2: 13;

          

           A26: (((b - x) |^ 0 ) / ( 0 ! )) = 1 by NEWTON: 4, NEWTON: 12;

          

          thus ( diff ((y * f),x)) = (( diff (y,(f . x))) * ( diff (f,x))) by A25, A24, FDIFF_2: 13

          .= (( diff (y,(f . x))) * ((f `| ].a, b.[) . x)) by A20, A23, FDIFF_1:def 7

          .= (( - 1) * ((( diff (f, ].a, b.[)) . ( 0 + 1)) . x)) by A14, A22

          .= ( - (((( diff (f, ].a, b.[)) . ( 0 + 1)) . x) * (((b - x) |^ 0 ) / ( 0 ! )))) by A26

          .= ( - ((((( diff (f, ].a, b.[)) . ( 0 + 1)) . x) * ((b - x) |^ 0 )) / ( 0 ! ))) by XCMPLX_1: 74;

        end;

        then for x be Real st x in ].a, b.[ holds (y * f) is_differentiable_in x;

        then

         A27: (y * f) is_differentiable_on ].a, b.[ by A19, A17, FDIFF_1: 9;

        

         A28: ( dom ((y * f) | [.a, b.])) = (( dom (y * f)) /\ [.a, b.]) by RELAT_1: 61

        .= [.a, b.] by A1, A4, A15, XBOOLE_1: 1, XBOOLE_1: 28

        .= (Z /\ [.a, b.]) by A4, XBOOLE_1: 28

        .= ( dom (g | [.a, b.])) by A9, RELAT_1: 61;

         A29:

        now

          let xx be object such that

           A30: xx in ( dom (g | [.a, b.]));

          reconsider x = xx as Real by A30;

          ( dom (g | [.a, b.])) = (( dom g) /\ [.a, b.]) by RELAT_1: 61;

          then ( dom (g | [.a, b.])) c= [.a, b.] by XBOOLE_1: 17;

          then

           A31: x in [.a, b.] by A30;

          

           A32: (((b - x) |^ 0 ) / ( 0 ! )) = 1 by NEWTON: 4, NEWTON: 12;

          

          thus ((g | [.a, b.]) . xx) = (g . x) by A30, FUNCT_1: 47

          .= ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . 0 )) by A4, A10, A31

          .= ((f . b) - (( Taylor (f,Z,x,b)) . 0 )) by SERIES_1:def 1

          .= ((f . b) - ((((( diff (f,Z)) . 0 ) . x) * ((b - x) |^ 0 )) / ( 0 ! ))) by Def7

          .= ((f . b) - ((((f | Z) . x) * ((b - x) |^ 0 )) / ( 0 ! ))) by Def5

          .= ((f . b) - (((f . x) * ((b - x) |^ 0 )) / ( 0 ! ))) by A4, A31, FUNCT_1: 49

          .= ((f . b) - ((f . x) * (((b - x) |^ 0 ) / ( 0 ! )))) by XCMPLX_1: 74

          .= (y . (f . x)) by A13, A32

          .= ((y * f) . x) by A18, A31, FUNCT_1: 13

          .= (((y * f) | [.a, b.]) . xx) by A28, A30, FUNCT_1: 47;

        end;

        ((f | Z) | [.a, b.]) is continuous by A5, Def5;

        then (((f | Z) | [.a, b.]) | [.a, b.]) is continuous by FCONT_1: 15;

        then ((f | [.a, b.]) | [.a, b.]) is continuous by A4, FUNCT_1: 51;

        then (f | [.a, b.]) is continuous by FCONT_1: 15;

        then ((y * f) | [.a, b.]) is continuous by A16, FCONT_1: 25;

        hence (g | [.a, b.]) is continuous by A28, A29, FUNCT_1: 2;

        

         A33: ( dom ((y * f) | ].a, b.[)) = (( dom (y * f)) /\ ].a, b.[) by RELAT_1: 61

        .= ].a, b.[ by A7, A18, A17, XBOOLE_1: 1, XBOOLE_1: 28

        .= (Z /\ ].a, b.[) by A4, A7, XBOOLE_1: 1, XBOOLE_1: 28

        .= ( dom (g | ].a, b.[)) by A9, RELAT_1: 61;

        now

          let xx be object such that

           A34: xx in ( dom (g | ].a, b.[));

          reconsider x = xx as Real by A34;

          ( dom (g | ].a, b.[)) = (( dom g) /\ ].a, b.[) by RELAT_1: 61;

          then ( dom (g | ].a, b.[)) c= ].a, b.[ by XBOOLE_1: 17;

          then

           A35: x in ].a, b.[ by A34;

          

           A36: (((b - x) |^ 0 ) / ( 0 ! )) = 1 by NEWTON: 4, NEWTON: 12;

          

          thus ((g | ].a, b.[) . xx) = (g . x) by A34, FUNCT_1: 47

          .= ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . 0 )) by A10, A8, A35

          .= ((f . b) - (( Taylor (f,Z,x,b)) . 0 )) by SERIES_1:def 1

          .= ((f . b) - ((((( diff (f,Z)) . 0 ) . x) * ((b - x) |^ 0 )) / ( 0 ! ))) by Def7

          .= ((f . b) - ((((f | Z) . x) * ((b - x) |^ 0 )) / ( 0 ! ))) by Def5

          .= ((f . b) - (((f . x) * ((b - x) |^ 0 )) / ( 0 ! ))) by A8, A35, FUNCT_1: 49

          .= ((f . b) - ((f . x) * (((b - x) |^ 0 ) / ( 0 ! )))) by XCMPLX_1: 74

          .= (y . (f . x)) by A13, A36

          .= ((y * f) . x) by A19, A35, FUNCT_1: 13

          .= (((y * f) | ].a, b.[) . xx) by A33, A34, FUNCT_1: 47;

        end;

        then

         A37: (g | ].a, b.[) = ((y * f) | ].a, b.[) by A33, FUNCT_1: 2;

        then (g | ].a, b.[) is_differentiable_on ].a, b.[ by A27, FDIFF_2: 16;

        then for x be Real st x in ].a, b.[ holds (g | ].a, b.[) is_differentiable_in x by FDIFF_1: 9;

        hence

         A38: g is_differentiable_on ].a, b.[ by A9, A8, FDIFF_1:def 6;

        now

          let x be Real such that

           A39: x in ].a, b.[;

          thus g is_differentiable_in x by A38, A39, FDIFF_1: 9;

          

          thus ( diff (g,x)) = ((g `| ].a, b.[) . x) by A38, A39, FDIFF_1:def 7

          .= (((g | ].a, b.[) `| ].a, b.[) . x) by A38, FDIFF_2: 16

          .= (((y * f) `| ].a, b.[) . x) by A37, A27, FDIFF_2: 16

          .= ( diff ((y * f),x)) by A27, A39, FDIFF_1:def 7

          .= ( - ((((( diff (f, ].a, b.[)) . ( 0 + 1)) . x) * ((b - x) |^ 0 )) / ( 0 ! ))) by A21, A39;

        end;

        hence thesis;

      end;

      

       A40: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A41: P[k];

        assume

         A42: f is_differentiable_on ((k + 1),Z);

        let a,b be Real such that

         A43: a < b and

         A44: [.a, b.] c= Z and

         A45: ((( diff (f,Z)) . (k + 1)) | [.a, b.]) is continuous and

         A46: f is_differentiable_on (((k + 1) + 1), ].a, b.[);

        (( diff (f,Z)) . k) is_differentiable_on Z by A42;

        then ((( diff (f,Z)) . k) | Z) is continuous by FDIFF_1: 25;

        then

         A47: ((( diff (f,Z)) . k) | [.a, b.]) is continuous by A44, FCONT_1: 16;

        

         A48: ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

        then

         A49: ].a, b.[ c= Z by A44, XBOOLE_1: 1;

        consider gk be PartFunc of REAL , REAL such that

         A50: ( dom gk) = Z and

         A51: for x be Real st x in Z holds (gk . x) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . k)) by Lm7;

        

         A52: f is_differentiable_on ((k + 1), ].a, b.[) by A46, Th23, NAT_1: 11;

        then

         A53: gk is_differentiable_on ].a, b.[ by A41, A42, A43, A44, A47, A50, A51, Th23, NAT_1: 11;

        

         A54: (gk | [.a, b.]) is continuous by A41, A42, A43, A44, A47, A52, A50, A51, Th23, NAT_1: 11;

        now

          

           A55: (( diff (f,Z)) . k) is_differentiable_on Z by A42;

          k <= (((k + 1) + 1) - 1) by NAT_1: 11;

          then

           A56: (( diff (f, ].a, b.[)) . k) is_differentiable_on ].a, b.[ by A46;

          

           A57: (( diff (f,Z)) . (k + 1)) = ((( diff (f,Z)) . k) `| Z) by Def5;

          let gk1 be PartFunc of REAL , REAL such that

           A58: ( dom gk1) = Z and

           A59: for x be Real st x in Z holds (gk1 . x) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . (k + 1)));

          

           A60: b in [.a, b.] by A43, XXREAL_1: 1;

          

          then (gk1 . b) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,b,b))) . (k + 1))) by A44, A59

          .= ((f . b) - ((( Partial_Sums ( Taylor (f,Z,b,b))) . k) + (( Taylor (f,Z,b,b)) . (k + 1)))) by SERIES_1:def 1

          .= (((f . b) - (( Partial_Sums ( Taylor (f,Z,b,b))) . k)) - (( Taylor (f,Z,b,b)) . (k + 1)))

          .= ((gk . b) - (( Taylor (f,Z,b,b)) . (k + 1))) by A44, A51, A60

          .= ( 0 - (( Taylor (f,Z,b,b)) . (k + 1))) by A41, A42, A43, A44, A47, A52, A50, A51, Th23, NAT_1: 11

          .= ( 0 - ((((( diff (f,Z)) . (k + 1)) . b) * ((b - b) |^ (k + 1))) / ((k + 1) ! ))) by Def7

          .= ( 0 - ((((( diff (f,Z)) . (k + 1)) . b) * (( 0 |^ k) * 0 )) / ((k + 1) ! ))) by NEWTON: 6

          .= 0 ;

          hence (gk1 . b) = 0 ;

          consider h be PartFunc of REAL , REAL such that

           A61: ( dom h) = ( [#] REAL ) and

           A62: for x be Real holds (h . x) = ((1 * ((b - x) |^ (k + 1))) / ((k + 1) ! )) and

           A63: for x be Real holds h is_differentiable_in x & ( diff (h,x)) = ( - ((1 * ((b - x) |^ k)) / (k ! ))) by Lm6;

          

           A64: ( dom ((( diff (f,Z)) . (k + 1)) (#) h)) = (( dom (( diff (f,Z)) . (k + 1))) /\ ( dom h)) by VALUED_1:def 4

          .= (Z /\ REAL ) by A61, A57, A55, FDIFF_1:def 7

          .= Z by XBOOLE_1: 28;

          

           A65: ( dom (gk - ((( diff (f,Z)) . (k + 1)) (#) h))) = (( dom gk) /\ ( dom ((( diff (f,Z)) . (k + 1)) (#) h))) by VALUED_1: 12

          .= Z by A50, A64;

          thus (gk1 | [.a, b.]) is continuous

          proof

            set ghk = (gk - ((( diff (f,Z)) . (k + 1)) (#) h));

            for x be Real st x in REAL holds h is_differentiable_in x by A63;

            then h is_differentiable_on REAL by A61, FDIFF_1: 9;

            then (h | REAL ) is continuous by FDIFF_1: 25;

            then

             A66: (h | [.a, b.]) is continuous by FCONT_1: 16;

            now

              let x be Element of REAL such that

               A67: x in Z;

              

              thus (gk1 . x) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . (k + 1))) by A59, A67

              .= ((f . b) - ((( Partial_Sums ( Taylor (f,Z,x,b))) . k) + (( Taylor (f,Z,x,b)) . (k + 1)))) by SERIES_1:def 1

              .= (((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . k)) - (( Taylor (f,Z,x,b)) . (k + 1)))

              .= ((gk . x) - (( Taylor (f,Z,x,b)) . (k + 1))) by A51, A67

              .= ((gk . x) - ((((( diff (f,Z)) . (k + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) ! ))) by Def7

              .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) . x) * ((1 * ((b - x) |^ (k + 1))) / ((k + 1) ! )))) by XCMPLX_1: 74

              .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) . x) * (h . x))) by A62

              .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) (#) h) . x)) by VALUED_1: 5

              .= ((gk - ((( diff (f,Z)) . (k + 1)) (#) h)) . x) by A65, A67, VALUED_1: 13;

            end;

            then

             A68: gk1 = ghk by A58, A65, PARTFUN1: 5;

             [.a, b.] c= ( dom (( diff (f,Z)) . (k + 1))) by A44, A57, A55, FDIFF_1:def 7;

            then (((( diff (f,Z)) . (k + 1)) (#) h) | ( [.a, b.] /\ [.a, b.])) is continuous by A45, A61, A66, FCONT_1: 19;

            hence thesis by A44, A50, A54, A64, A68, FCONT_1: 19;

          end;

          

           A69: (( diff (f, ].a, b.[)) . (k + 1)) = ((( diff (f, ].a, b.[)) . k) `| ].a, b.[) by Def5;

          set gfh = (gk - ((( diff (f, ].a, b.[)) . (k + 1)) (#) h));

          

           A70: ( dom ((( diff (f, ].a, b.[)) . (k + 1)) (#) h)) = (( dom (( diff (f, ].a, b.[)) . (k + 1))) /\ ( dom h)) by VALUED_1:def 4

          .= ( ].a, b.[ /\ REAL ) by A61, A69, A56, FDIFF_1:def 7

          .= ].a, b.[ by XBOOLE_1: 28;

          

          then

           A71: ( dom (gk - ((( diff (f, ].a, b.[)) . (k + 1)) (#) h))) = (Z /\ ].a, b.[) by A50, VALUED_1: 12

          .= ].a, b.[ by A44, A48, XBOOLE_1: 1, XBOOLE_1: 28;

          

           A72: for x be Real st x in ].a, b.[ holds ((gk - ((( diff (f,Z)) . (k + 1)) (#) h)) . x) = ((gk - ((( diff (f, ].a, b.[)) . (k + 1)) (#) h)) . x)

          proof

            let x be Real such that

             A73: x in ].a, b.[;

            

            thus ((gk - ((( diff (f, ].a, b.[)) . (k + 1)) (#) h)) . x) = ((gk . x) - (((( diff (f, ].a, b.[)) . (k + 1)) (#) h) . x)) by A71, A73, VALUED_1: 13

            .= ((gk . x) - (((( diff (f, ].a, b.[)) . (k + 1)) . x) * (h . x))) by VALUED_1: 5

            .= ((gk . x) - ((((( diff (f,Z)) . (k + 1)) | ].a, b.[) . x) * (h . x))) by A42, A43, A44, A48, Th24, XBOOLE_1: 1

            .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) . x) * (h . x))) by A73, FUNCT_1: 49

            .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) (#) h) . x)) by VALUED_1: 5

            .= ((gk - ((( diff (f,Z)) . (k + 1)) (#) h)) . x) by A49, A65, A73, VALUED_1: 13;

          end;

           A74:

          now

            let xx be object such that

             A75: xx in ( dom gfh);

            reconsider x = xx as Real by A75;

            

            thus (gk1 . xx) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . (k + 1))) by A49, A59, A71, A75

            .= ((f . b) - ((( Partial_Sums ( Taylor (f,Z,x,b))) . k) + (( Taylor (f,Z,x,b)) . (k + 1)))) by SERIES_1:def 1

            .= (((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . k)) - (( Taylor (f,Z,x,b)) . (k + 1)))

            .= ((gk . x) - (( Taylor (f,Z,x,b)) . (k + 1))) by A49, A51, A71, A75

            .= ((gk . x) - ((((( diff (f,Z)) . (k + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) ! ))) by Def7

            .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) . x) * ((1 * ((b - x) |^ (k + 1))) / ((k + 1) ! )))) by XCMPLX_1: 74

            .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) . x) * (h . x))) by A62

            .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) (#) h) . x)) by VALUED_1: 5

            .= ((gk - ((( diff (f,Z)) . (k + 1)) (#) h)) . x) by A49, A65, A71, A75, VALUED_1: 13

            .= (gfh . xx) by A71, A72, A75;

          end;

          

           A76: (( diff (f, ].a, b.[)) . (k + 1)) is_differentiable_on ].a, b.[ by A46;

          for x be Real st x in ].a, b.[ holds h is_differentiable_in x by A63;

          then

           A77: h is_differentiable_on ].a, b.[ by A61, FDIFF_1: 9;

          then

           A78: ((( diff (f, ].a, b.[)) . (k + 1)) (#) h) is_differentiable_on ].a, b.[ by A70, A76, FDIFF_1: 21;

          then

           A79: gfh is_differentiable_on ].a, b.[ by A53, A71, FDIFF_1: 19;

          ( dom gfh) = (( dom gk1) /\ ].a, b.[) by A44, A48, A58, A71, XBOOLE_1: 1, XBOOLE_1: 28;

          then

           A80: ((gk1 | ].a, b.[) | ].a, b.[) = (gfh | ].a, b.[) by A74, FUNCT_1: 46;

          then (gfh | ].a, b.[) = (gk1 | ].a, b.[) by FUNCT_1: 51;

          then for x be Real st x in ].a, b.[ holds (gk1 | ].a, b.[) is_differentiable_in x by A79, FDIFF_1:def 6;

          hence

           A81: gk1 is_differentiable_on ].a, b.[ by A49, A58, FDIFF_1:def 6;

          now

            let x be Real such that

             A82: x in ].a, b.[;

            

            thus ( diff (gk1,x)) = ((gk1 `| ].a, b.[) . x) by A81, A82, FDIFF_1:def 7

            .= (((gk1 | ].a, b.[) `| ].a, b.[) . x) by A81, FDIFF_2: 16

            .= (((gfh | ].a, b.[) `| ].a, b.[) . x) by A80, FUNCT_1: 51

            .= ((gfh `| ].a, b.[) . x) by A79, FDIFF_2: 16

            .= (( diff (gk,x)) - ( diff (((( diff (f, ].a, b.[)) . (k + 1)) (#) h),x))) by A53, A71, A78, A82, FDIFF_1: 19

            .= (( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k ! ))) - ( diff (((( diff (f, ].a, b.[)) . (k + 1)) (#) h),x))) by A41, A42, A43, A44, A47, A52, A50, A51, A82, Th23, NAT_1: 11

            .= (( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k ! ))) - ((((( diff (f, ].a, b.[)) . (k + 1)) (#) h) `| ].a, b.[) . x)) by A78, A82, FDIFF_1:def 7

            .= (( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k ! ))) - (((h . x) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x))) + (((( diff (f, ].a, b.[)) . (k + 1)) . x) * ( diff (h,x))))) by A70, A76, A77, A82, FDIFF_1: 21

            .= ((( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k ! ))) - ((h . x) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x)))) - (((( diff (f, ].a, b.[)) . (k + 1)) . x) * ( diff (h,x))))

            .= ((( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k ! ))) - (((1 * ((b - x) |^ (k + 1))) / ((k + 1) ! )) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x)))) - (((( diff (f, ].a, b.[)) . (k + 1)) . x) * ( diff (h,x)))) by A62

            .= ((( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k ! ))) - ((((b - x) |^ (k + 1)) / ((k + 1) ! )) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x)))) - (((( diff (f, ].a, b.[)) . (k + 1)) . x) * ( - ((1 * ((b - x) |^ k)) / (k ! ))))) by A63

            .= ((( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k ! ))) + (((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((1 * ((b - x) |^ k)) / (k ! )))) - ((((b - x) |^ (k + 1)) / ((k + 1) ! )) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x))))

            .= ((( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k ! ))) + ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k ! ))) - ((((b - x) |^ (k + 1)) / ((k + 1) ! )) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x)))) by XCMPLX_1: 74

            .= ( - ((((b - x) |^ (k + 1)) / ((k + 1) ! )) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x))))

            .= ( - ((((b - x) |^ (k + 1)) / ((k + 1) ! )) * (((( diff (f, ].a, b.[)) . (k + 1)) `| ].a, b.[) . x))) by A76, A82, FDIFF_1:def 7

            .= ( - ((((b - x) |^ (k + 1)) / ((k + 1) ! )) * ((( diff (f, ].a, b.[)) . ((k + 1) + 1)) . x))) by Def5

            .= ( - ((((( diff (f, ].a, b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) ! ))) by XCMPLX_1: 74;

          end;

          hence for x be Real st x in ].a, b.[ holds ( diff (gk1,x)) = ( - ((((( diff (f, ].a, b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) ! )));

        end;

        hence thesis;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A2, A40);

      hence thesis;

    end;

    

     Lm9: for n be Nat holds for f be PartFunc of REAL , REAL holds for Z be Subset of REAL st Z c= ( dom f) & f is_differentiable_on (n,Z) holds for a,b be Real st a < b & [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[) holds ex g be PartFunc of REAL , REAL st ( dom g) = Z & (for x be Real st x in Z holds (g . x) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . n))) & (g . b) = 0 & (g | [.a, b.]) is continuous & g is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (g,x)) = ( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! )))

    proof

      let n be Nat;

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL such that

       A1: Z c= ( dom f) & f is_differentiable_on (n,Z);

      let a,b be Real such that

       A2: a < b & [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[);

      consider g be PartFunc of REAL , REAL such that

       A3: ( dom g) = Z & for x be Real st x in Z holds (g . x) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . n)) by Lm7;

      take g;

      thus thesis by A1, A2, A3, Lm8;

    end;

    theorem :: TAYLOR_1:25

    

     Th25: for n be Nat, f be PartFunc of REAL , REAL , Z be Subset of REAL st Z c= ( dom f) & f is_differentiable_on (n,Z) holds for a,b be Real st a < b & [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[) holds for l be Real, g be PartFunc of REAL , REAL st ( dom g) = ( [#] REAL ) & (for x be Real holds (g . x) = (((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) ! )))) & (((f . b) - (( Partial_Sums ( Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) ! ))) = 0 holds g is_differentiable_on ].a, b.[ & (g . a) = 0 & (g . b) = 0 & (g | [.a, b.]) is continuous & for x be Real st x in ].a, b.[ holds ( diff (g,x)) = (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! ))) + ((l * ((b - x) |^ n)) / (n ! )))

    proof

      let n be Nat;

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL such that

       A1: Z c= ( dom f) & f is_differentiable_on (n,Z);

      let a,b be Real such that

       A2: a < b and

       A3: [.a, b.] c= Z and

       A4: ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[);

      let l be Real;

      consider p be PartFunc of REAL , REAL such that

       A5: ( dom p) = ( [#] REAL ) and

       A6: for x be Real holds (p . x) = ((l * ((b - x) |^ (n + 1))) / ((n + 1) ! )) and

       A7: for x be Real holds p is_differentiable_in x & ( diff (p,x)) = ( - ((l * ((b - x) |^ n)) / (n ! ))) by Lm6;

      consider h be PartFunc of REAL , REAL such that

       A8: ( dom h) = Z and

       A9: for x be Real st x in Z holds (h . x) = ((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . n)) and

       A10: (h . b) = 0 and

       A11: (h | [.a, b.]) is continuous and

       A12: h is_differentiable_on ].a, b.[ and

       A13: for x be Real st x in ].a, b.[ holds ( diff (h,x)) = ( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! ))) by A1, A2, A3, A4, Lm9;

      

       A14: [.a, b.] c= (( dom h) /\ ( dom p)) by A3, A8, A5, XBOOLE_1: 19;

      let g be PartFunc of REAL , REAL such that

       A15: ( dom g) = ( [#] REAL ) and

       A16: for x be Real holds (g . x) = (((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) ! ))) and

       A17: (((f . b) - (( Partial_Sums ( Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) ! ))) = 0 ;

      set hp = (h - p);

      

       A18: ( dom hp) = (( dom h) /\ ( dom p)) by VALUED_1: 12

      .= Z by A8, A5, XBOOLE_1: 28;

      

       A19: for x be object st x in ( dom hp) holds (hp . x) = (g . x)

      proof

        let x be object such that

         A20: x in ( dom hp);

        reconsider xx = x as Real by A20;

        

        thus (hp . x) = ((h . xx) - (p . xx)) by A20, VALUED_1: 13

        .= (((f . b) - (( Partial_Sums ( Taylor (f,Z,xx,b))) . n)) - (p . xx)) by A9, A18, A20

        .= (((f . b) - (( Partial_Sums ( Taylor (f,Z,xx,b))) . n)) - ((l * ((b - xx) |^ (n + 1))) / ((n + 1) ! ))) by A6

        .= (g . x) by A16;

      end;

      for x be Real st x in REAL holds p is_differentiable_in x by A7;

      then p is_differentiable_on REAL by A5, FDIFF_1: 9;

      then (p | REAL ) is continuous by FDIFF_1: 25;

      then

       A21: (p | [.a, b.]) is continuous by FCONT_1: 16;

       ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

      then

       A22: ].a, b.[ c= Z by A3, XBOOLE_1: 1;

      

       A23: ( dom hp) = (( dom g) /\ Z) by A15, A18, XBOOLE_1: 28;

      

      then

       A24: (hp | ].a, b.[) = ((g | Z) | ].a, b.[) by A19, FUNCT_1: 46

      .= (g | ].a, b.[) by A22, FUNCT_1: 51;

      

       A25: for x be Real st x in ].a, b.[ holds hp is_differentiable_in x & ( diff (hp,x)) = (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! ))) + ((l * ((b - x) |^ n)) / (n ! )))

      proof

        let x be Real such that

         A26: x in ].a, b.[;

        

         A27: h is_differentiable_in x by A12, A26, FDIFF_1: 9;

        

         A28: p is_differentiable_in x by A7;

        hence hp is_differentiable_in x by A27, FDIFF_1: 14;

        

        thus ( diff (hp,x)) = (( diff (h,x)) - ( diff (p,x))) by A27, A28, FDIFF_1: 14

        .= (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! ))) - ( diff (p,x))) by A13, A26

        .= (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! ))) - ( - ((l * ((b - x) |^ n)) / (n ! )))) by A7

        .= (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! ))) + ((l * ((b - x) |^ n)) / (n ! )));

      end;

      then for x be Real st x in ].a, b.[ holds hp is_differentiable_in x;

      then

       A29: hp is_differentiable_on ].a, b.[ by A18, A22, FDIFF_1: 9;

      then for x be Real st x in ].a, b.[ holds (hp | ].a, b.[) is_differentiable_in x by FDIFF_1:def 6;

      hence

       A30: g is_differentiable_on ].a, b.[ by A15, A24, FDIFF_1:def 6;

      reconsider aa = a as Real;

      (g . aa) = 0 by A16, A17;

      hence (g . a) = 0 ;

      

       A31: b in [.a, b.] by A2, XXREAL_1: 1;

      

      then (g . b) = (hp . b) by A3, A18, A19

      .= ((h . b) - (p . b)) by A3, A18, A31, VALUED_1: 13

      .= ( 0 - ((l * ((b - b) |^ (n + 1))) / ((n + 1) ! ))) by A10, A6

      .= ( 0 - ((l * (( 0 |^ n) * 0 )) / ((n + 1) ! ))) by NEWTON: 6

      .= 0 ;

      hence (g . b) = 0 ;

      (hp | [.a, b.]) = ((g | Z) | [.a, b.]) by A23, A19, FUNCT_1: 46

      .= (g | [.a, b.]) by A3, FUNCT_1: 51;

      hence (g | [.a, b.]) is continuous by A11, A14, A21, FCONT_1: 18;

      thus for x be Real st x in ].a, b.[ holds ( diff (g,x)) = (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! ))) + ((l * ((b - x) |^ n)) / (n ! )))

      proof

        let x be Real such that

         A32: x in ].a, b.[;

        

        thus ( diff (g,x)) = ((g `| ].a, b.[) . x) by A30, A32, FDIFF_1:def 7

        .= (((g | ].a, b.[) `| ].a, b.[) . x) by A30, FDIFF_2: 16

        .= ((hp `| ].a, b.[) . x) by A24, A29, FDIFF_2: 16

        .= ( diff (hp,x)) by A29, A32, FDIFF_1:def 7

        .= (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n ! ))) + ((l * ((b - x) |^ n)) / (n ! ))) by A25, A32;

      end;

    end;

    theorem :: TAYLOR_1:26

    

     Th26: for n be Nat, f be PartFunc of REAL , REAL , Z be Subset of REAL , b,l be Real holds ex g be Function of REAL , REAL st for x be Real holds (g . x) = (((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) ! )))

    proof

      let n be Nat;

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL ;

      let b,l be Real;

      deffunc U( Real) = ( In ((((f . b) - (( Partial_Sums ( Taylor (f,Z,$1,b))) . n)) - ((l * ((b - $1) |^ (n + 1))) / ((n + 1) ! ))), REAL ));

      consider g be Function of REAL , REAL such that

       A1: for d be Element of REAL holds (g . d) = U(d) from FUNCT_2:sch 4;

      take g;

      let x be Real;

      reconsider x as Element of REAL by XREAL_0:def 1;

      (g . x) = U(x) by A1;

      hence thesis;

    end;

    theorem :: TAYLOR_1:27

    

     Th27: for n be Nat, f be PartFunc of REAL , REAL , Z be Subset of REAL st Z c= ( dom f) & f is_differentiable_on (n,Z) holds for a,b be Real st a < b & [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[) holds ex c be Real st c in ].a, b.[ & (f . b) = ((( Partial_Sums ( Taylor (f,Z,a,b))) . n) + ((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )))

    proof

      let n be Nat;

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL such that

       A1: Z c= ( dom f) & f is_differentiable_on (n,Z);

      let a,b be Real such that

       A2: a < b and

       A3: [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[);

      (b - a) <> 0 by A2;

      then

       A4: ((b - a) |^ (n + 1)) <> 0 by CARD_4: 3;

      deffunc F( Real) = ( In (((f . b) - (( Partial_Sums ( Taylor (f,Z,$1,b))) . n)), REAL ));

      reconsider l = ( F(a) / (((b - a) |^ (n + 1)) / ((n + 1) ! ))) as Real;

      consider g be Function of REAL , REAL such that

       A5: for x be Real holds (g . x) = (((f . b) - (( Partial_Sums ( Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) ! ))) by Th26;

      

       A6: (((f . b) - (( Partial_Sums ( Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) ! ))) = ( F(a) - (( F(a) / (((b - a) |^ (n + 1)) / ((n + 1) ! ))) * (((b - a) |^ (n + 1)) / ((n + 1) ! )))) by XCMPLX_1: 74

      .= ( F(a) - F(a)) by A4, XCMPLX_1: 50, XCMPLX_1: 87

      .= 0 ;

      then

       A7: (g . a) = 0 by A5;

      

       A8: ( dom g) = REAL by FUNCT_2:def 1;

      then

       A9: (g | [.a, b.]) is continuous by A1, A2, A3, A5, A6, Th25;

      g is_differentiable_on ].a, b.[ & (g . b) = 0 by A1, A2, A3, A5, A6, A8, Th25;

      then

      consider c be Real such that

       A10: c in ].a, b.[ and

       A11: ( diff (g,c)) = 0 by A2, A8, A7, A9, ROLLE: 1;

      c in { r where r be Real : a < r & r < b } by A10, RCOMP_1:def 2;

      then ex r be Real st c = r & a < r & r < b;

      then (b - c) <> 0 ;

      then

       A12: ((b - c) |^ n) <> 0 by CARD_4: 3;

      ( dom g) = REAL by FUNCT_2:def 1;

      then (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((b - c) |^ n)) / (n ! ))) + ((l * ((b - c) |^ n)) / (n ! ))) = 0 by A1, A2, A3, A5, A6, A10, A11, Th25;

      then ((((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((b - c) |^ n)) / (n ! )) * (n ! )) - (((l * ((b - c) |^ n)) / (n ! )) * (n ! ))) = 0 ;

      then ((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((b - c) |^ n)) - (((l * ((b - c) |^ n)) / (n ! )) * (n ! ))) = 0 by XCMPLX_1: 87;

      then (((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((b - c) |^ n)) - (l * ((b - c) |^ n))) / ((b - c) |^ n)) = ( 0 / ((b - c) |^ n)) by XCMPLX_1: 87;

      then (((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((b - c) |^ n)) / ((b - c) |^ n)) - ((l * ((b - c) |^ n)) / ((b - c) |^ n))) = 0 by XCMPLX_1: 120;

      then (((( diff (f, ].a, b.[)) . (n + 1)) . c) - ((l * ((b - c) |^ n)) / ((b - c) |^ n))) = 0 by A12, XCMPLX_1: 89;

      then (((f . b) - (( Partial_Sums ( Taylor (f,Z,a,b))) . n)) - ((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! ))) = 0 by A6, A12, XCMPLX_1: 89;

      then (f . b) = (((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) ! )) + (( Partial_Sums ( Taylor (f,Z,a,b))) . n));

      hence thesis by A10;

    end;

    

     Lm10: for f be PartFunc of REAL , REAL holds for Z be Subset of REAL st Z c= ( dom f) holds for n be Nat st f is_differentiable_on (n,Z) holds for a,b be Real st a < b & [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[) holds for g be PartFunc of REAL , REAL st ( dom g) = Z & for x be Real st x in Z holds (g . x) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . n)) holds (g . a) = 0 & (g | [.a, b.]) is continuous & g is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (g,x)) = ( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n ! )))

    proof

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL such that

       A1: Z c= ( dom f);

      defpred P[ Nat] means f is_differentiable_on ($1,Z) implies for a,b be Real st a < b & [.a, b.] c= Z & ((( diff (f,Z)) . $1) | [.a, b.]) is continuous & f is_differentiable_on (($1 + 1), ].a, b.[) holds for g be PartFunc of REAL , REAL st ( dom g) = Z & for x be Real st x in Z holds (g . x) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . $1)) holds (g . a) = 0 & (g | [.a, b.]) is continuous & g is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (g,x)) = ( - ((((( diff (f, ].a, b.[)) . ($1 + 1)) . x) * ((a - x) |^ $1)) / ($1 ! )));

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A3: P[k];

        assume

         A4: f is_differentiable_on ((k + 1),Z);

        let a,b be Real such that

         A5: a < b and

         A6: [.a, b.] c= Z and

         A7: ((( diff (f,Z)) . (k + 1)) | [.a, b.]) is continuous and

         A8: f is_differentiable_on (((k + 1) + 1), ].a, b.[);

        (( diff (f,Z)) . k) is_differentiable_on Z by A4;

        then ((( diff (f,Z)) . k) | Z) is continuous by FDIFF_1: 25;

        then

         A9: ((( diff (f,Z)) . k) | [.a, b.]) is continuous by A6, FCONT_1: 16;

        

         A10: ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

        then

         A11: ].a, b.[ c= Z by A6, XBOOLE_1: 1;

        consider gk be PartFunc of REAL , REAL such that

         A12: ( dom gk) = Z and

         A13: for x be Real st x in Z holds (gk . x) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . k)) by Lm7;

        

         A14: f is_differentiable_on ((k + 1), ].a, b.[) by A8, Th23, NAT_1: 11;

        then

         A15: gk is_differentiable_on ].a, b.[ by A3, A4, A5, A6, A9, A12, A13, Th23, NAT_1: 11;

        

         A16: (gk | [.a, b.]) is continuous by A3, A4, A5, A6, A9, A14, A12, A13, Th23, NAT_1: 11;

        now

          

           A17: (( diff (f,Z)) . k) is_differentiable_on Z by A4;

          k <= (((k + 1) + 1) - 1) by NAT_1: 11;

          then

           A18: (( diff (f, ].a, b.[)) . k) is_differentiable_on ].a, b.[ by A8;

          

           A19: (( diff (f,Z)) . (k + 1)) = ((( diff (f,Z)) . k) `| Z) by Def5;

          let gk1 be PartFunc of REAL , REAL such that

           A20: ( dom gk1) = Z and

           A21: for x be Real st x in Z holds (gk1 . x) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . (k + 1)));

          

           A22: a in [.a, b.] by A5, XXREAL_1: 1;

          

          then (gk1 . a) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,a,a))) . (k + 1))) by A6, A21

          .= ((f . a) - ((( Partial_Sums ( Taylor (f,Z,a,a))) . k) + (( Taylor (f,Z,a,a)) . (k + 1)))) by SERIES_1:def 1

          .= (((f . a) - (( Partial_Sums ( Taylor (f,Z,a,a))) . k)) - (( Taylor (f,Z,a,a)) . (k + 1)))

          .= ((gk . a) - (( Taylor (f,Z,a,a)) . (k + 1))) by A6, A13, A22

          .= ( 0 - (( Taylor (f,Z,a,a)) . (k + 1))) by A3, A4, A5, A6, A9, A14, A12, A13, Th23, NAT_1: 11

          .= ( 0 - ((((( diff (f,Z)) . (k + 1)) . a) * ((a - a) |^ (k + 1))) / ((k + 1) ! ))) by Def7

          .= ( 0 - ((((( diff (f,Z)) . (k + 1)) . a) * (( 0 |^ k) * 0 )) / ((k + 1) ! ))) by NEWTON: 6

          .= 0 ;

          hence (gk1 . a) = 0 ;

          consider h be PartFunc of REAL , REAL such that

           A23: ( dom h) = ( [#] REAL ) and

           A24: for x be Real holds (h . x) = ((1 * ((a - x) |^ (k + 1))) / ((k + 1) ! )) and

           A25: for x be Real holds h is_differentiable_in x & ( diff (h,x)) = ( - ((1 * ((a - x) |^ k)) / (k ! ))) by Lm6;

          

           A26: ( dom ((( diff (f,Z)) . (k + 1)) (#) h)) = (( dom (( diff (f,Z)) . (k + 1))) /\ ( dom h)) by VALUED_1:def 4

          .= (Z /\ REAL ) by A23, A19, A17, FDIFF_1:def 7

          .= Z by XBOOLE_1: 28;

          

           A27: ( dom (gk - ((( diff (f,Z)) . (k + 1)) (#) h))) = (( dom gk) /\ ( dom ((( diff (f,Z)) . (k + 1)) (#) h))) by VALUED_1: 12

          .= Z by A12, A26;

          thus (gk1 | [.a, b.]) is continuous

          proof

            set ghk = (gk - ((( diff (f,Z)) . (k + 1)) (#) h));

            for x be Real st x in REAL holds h is_differentiable_in x by A25;

            then h is_differentiable_on REAL by A23, FDIFF_1: 9;

            then (h | REAL ) is continuous by FDIFF_1: 25;

            then

             A28: (h | [.a, b.]) is continuous by FCONT_1: 16;

            now

              let x be Element of REAL such that

               A29: x in Z;

              

              thus (gk1 . x) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . (k + 1))) by A21, A29

              .= ((f . a) - ((( Partial_Sums ( Taylor (f,Z,x,a))) . k) + (( Taylor (f,Z,x,a)) . (k + 1)))) by SERIES_1:def 1

              .= (((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . k)) - (( Taylor (f,Z,x,a)) . (k + 1)))

              .= ((gk . x) - (( Taylor (f,Z,x,a)) . (k + 1))) by A13, A29

              .= ((gk . x) - ((((( diff (f,Z)) . (k + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) ! ))) by Def7

              .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) . x) * ((1 * ((a - x) |^ (k + 1))) / ((k + 1) ! )))) by XCMPLX_1: 74

              .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) . x) * (h . x))) by A24

              .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) (#) h) . x)) by VALUED_1: 5

              .= ((gk - ((( diff (f,Z)) . (k + 1)) (#) h)) . x) by A27, A29, VALUED_1: 13;

            end;

            then

             A30: gk1 = ghk by A20, A27, PARTFUN1: 5;

             [.a, b.] c= ( dom (( diff (f,Z)) . (k + 1))) by A6, A19, A17, FDIFF_1:def 7;

            then (((( diff (f,Z)) . (k + 1)) (#) h) | ( [.a, b.] /\ [.a, b.])) is continuous by A7, A23, A28, FCONT_1: 19;

            hence thesis by A6, A12, A16, A26, A30, FCONT_1: 19;

          end;

          

           A31: (( diff (f, ].a, b.[)) . (k + 1)) = ((( diff (f, ].a, b.[)) . k) `| ].a, b.[) by Def5;

          set gfh = (gk - ((( diff (f, ].a, b.[)) . (k + 1)) (#) h));

          

           A32: ( dom ((( diff (f, ].a, b.[)) . (k + 1)) (#) h)) = (( dom (( diff (f, ].a, b.[)) . (k + 1))) /\ ( dom h)) by VALUED_1:def 4

          .= ( ].a, b.[ /\ REAL ) by A23, A31, A18, FDIFF_1:def 7

          .= ].a, b.[ by XBOOLE_1: 28;

          

           A33: ( dom (gk - ((( diff (f, ].a, b.[)) . (k + 1)) (#) h))) = (Z /\ ( dom ((( diff (f, ].a, b.[)) . (k + 1)) (#) h))) by A12, VALUED_1: 12

          .= ].a, b.[ by A6, A10, A32, XBOOLE_1: 1, XBOOLE_1: 28;

          

           A34: for x be Real st x in ].a, b.[ holds ((gk - ((( diff (f,Z)) . (k + 1)) (#) h)) . x) = ((gk - ((( diff (f, ].a, b.[)) . (k + 1)) (#) h)) . x)

          proof

            let x be Real such that

             A35: x in ].a, b.[;

            

            thus ((gk - ((( diff (f, ].a, b.[)) . (k + 1)) (#) h)) . x) = ((gk . x) - (((( diff (f, ].a, b.[)) . (k + 1)) (#) h) . x)) by A33, A35, VALUED_1: 13

            .= ((gk . x) - (((( diff (f, ].a, b.[)) . (k + 1)) . x) * (h . x))) by VALUED_1: 5

            .= ((gk . x) - ((((( diff (f,Z)) . (k + 1)) | ].a, b.[) . x) * (h . x))) by A4, A5, A6, A10, Th24, XBOOLE_1: 1

            .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) . x) * (h . x))) by A35, FUNCT_1: 49

            .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) (#) h) . x)) by VALUED_1: 5

            .= ((gk - ((( diff (f,Z)) . (k + 1)) (#) h)) . x) by A11, A27, A35, VALUED_1: 13;

          end;

           A36:

          now

            let xx be object such that

             A37: xx in ( dom gfh);

            reconsider x = xx as Real by A37;

            

            thus (gk1 . xx) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . (k + 1))) by A11, A21, A33, A37

            .= ((f . a) - ((( Partial_Sums ( Taylor (f,Z,x,a))) . k) + (( Taylor (f,Z,x,a)) . (k + 1)))) by SERIES_1:def 1

            .= (((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . k)) - (( Taylor (f,Z,x,a)) . (k + 1)))

            .= ((gk . x) - (( Taylor (f,Z,x,a)) . (k + 1))) by A11, A13, A33, A37

            .= ((gk . x) - ((((( diff (f,Z)) . (k + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) ! ))) by Def7

            .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) . x) * ((1 * ((a - x) |^ (k + 1))) / ((k + 1) ! )))) by XCMPLX_1: 74

            .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) . x) * (h . x))) by A24

            .= ((gk . x) - (((( diff (f,Z)) . (k + 1)) (#) h) . x)) by VALUED_1: 5

            .= ((gk - ((( diff (f,Z)) . (k + 1)) (#) h)) . x) by A11, A27, A33, A37, VALUED_1: 13

            .= (gfh . xx) by A33, A34, A37;

          end;

          

           A38: (( diff (f, ].a, b.[)) . (k + 1)) is_differentiable_on ].a, b.[ by A8;

          for x be Real st x in ].a, b.[ holds h is_differentiable_in x by A25;

          then

           A39: h is_differentiable_on ].a, b.[ by A23, FDIFF_1: 9;

          then

           A40: ((( diff (f, ].a, b.[)) . (k + 1)) (#) h) is_differentiable_on ].a, b.[ by A32, A38, FDIFF_1: 21;

          then

           A41: gfh is_differentiable_on ].a, b.[ by A15, A33, FDIFF_1: 19;

          ( dom gfh) = (( dom gk1) /\ ].a, b.[) by A6, A10, A20, A33, XBOOLE_1: 1, XBOOLE_1: 28;

          then

           A42: ((gk1 | ].a, b.[) | ].a, b.[) = (gfh | ].a, b.[) by A36, FUNCT_1: 46;

          then (gfh | ].a, b.[) = (gk1 | ].a, b.[) by FUNCT_1: 51;

          then for x be Real st x in ].a, b.[ holds (gk1 | ].a, b.[) is_differentiable_in x by A41, FDIFF_1:def 6;

          hence

           A43: gk1 is_differentiable_on ].a, b.[ by A11, A20, FDIFF_1:def 6;

          now

            let x be Real such that

             A44: x in ].a, b.[;

            

            thus ( diff (gk1,x)) = ((gk1 `| ].a, b.[) . x) by A43, A44, FDIFF_1:def 7

            .= (((gk1 | ].a, b.[) `| ].a, b.[) . x) by A43, FDIFF_2: 16

            .= (((gfh | ].a, b.[) `| ].a, b.[) . x) by A42, FUNCT_1: 51

            .= ((gfh `| ].a, b.[) . x) by A41, FDIFF_2: 16

            .= (( diff (gk,x)) - ( diff (((( diff (f, ].a, b.[)) . (k + 1)) (#) h),x))) by A15, A33, A40, A44, FDIFF_1: 19

            .= (( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - ( diff (((( diff (f, ].a, b.[)) . (k + 1)) (#) h),x))) by A3, A4, A5, A6, A9, A14, A12, A13, A44, Th23, NAT_1: 11

            .= (( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - ((((( diff (f, ].a, b.[)) . (k + 1)) (#) h) `| ].a, b.[) . x)) by A40, A44, FDIFF_1:def 7

            .= (( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - (((h . x) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x))) + (((( diff (f, ].a, b.[)) . (k + 1)) . x) * ( diff (h,x))))) by A32, A38, A39, A44, FDIFF_1: 21

            .= ((( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - ((h . x) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x)))) - (((( diff (f, ].a, b.[)) . (k + 1)) . x) * ( diff (h,x))))

            .= ((( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - (((1 * ((a - x) |^ (k + 1))) / ((k + 1) ! )) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x)))) - (((( diff (f, ].a, b.[)) . (k + 1)) . x) * ( diff (h,x)))) by A24

            .= ((( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x)))) - (((( diff (f, ].a, b.[)) . (k + 1)) . x) * ( - ((1 * ((a - x) |^ k)) / (k ! ))))) by A25

            .= ((( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) + (((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((1 * ((a - x) |^ k)) / (k ! )))) - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x))))

            .= ((( - ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) + ((((( diff (f, ].a, b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x)))) by XCMPLX_1: 74

            .= ( - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * ( diff ((( diff (f, ].a, b.[)) . (k + 1)),x))))

            .= ( - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * (((( diff (f, ].a, b.[)) . (k + 1)) `| ].a, b.[) . x))) by A38, A44, FDIFF_1:def 7

            .= ( - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * ((( diff (f, ].a, b.[)) . ((k + 1) + 1)) . x))) by Def5

            .= ( - ((((( diff (f, ].a, b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) ! ))) by XCMPLX_1: 74;

          end;

          hence for x be Real st x in ].a, b.[ holds ( diff (gk1,x)) = ( - ((((( diff (f, ].a, b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) ! )));

        end;

        hence thesis;

      end;

      

       A45: P[ 0 ]

      proof

        assume f is_differentiable_on ( 0 ,Z);

        let a,b be Real such that

         A46: a < b and

         A47: [.a, b.] c= Z and

         A48: ((( diff (f,Z)) . 0 ) | [.a, b.]) is continuous and

         A49: f is_differentiable_on (( 0 + 1), ].a, b.[);

        

         A50: ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

        then

         A51: ].a, b.[ c= Z by A47, XBOOLE_1: 1;

        let g be PartFunc of REAL , REAL such that

         A52: ( dom g) = Z and

         A53: for x be Real st x in Z holds (g . x) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . 0 ));

        

         A54: a in [.a, b.] by A46, XXREAL_1: 1;

        

        hence (g . a) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,a,a))) . 0 )) by A47, A53

        .= ((f . a) - (( Taylor (f,Z,a,a)) . 0 )) by SERIES_1:def 1

        .= ((f . a) - ((((( diff (f,Z)) . 0 ) . a) * ((a - a) |^ 0 )) / ( 0 ! ))) by Def7

        .= ((f . a) - ((((f | Z) . a) * ((a - a) |^ 0 )) / ( 0 ! ))) by Def5

        .= ((f . a) - (((f . a) * ((a - a) |^ 0 )) / ( 0 ! ))) by A47, A54, FUNCT_1: 49

        .= ((f . a) - ((f . a) * 1)) by NEWTON: 4, NEWTON: 12

        .= 0 ;

        consider y be PartFunc of REAL , REAL such that

         A55: ( dom y) = ( [#] REAL ) and

         A56: for x be Real holds (y . x) = ((f . a) - x) and

         A57: for x be Real holds y is_differentiable_in x & ( diff (y,x)) = ( - 1) by Lm5;

        ( rng f) c= REAL ;

        then

         A58: ( dom (y * f)) = ( dom f) by A55, RELAT_1: 27;

        for x be Real st x in REAL holds y is_differentiable_in x by A57;

        then y is_differentiable_on REAL by A55, FDIFF_1: 9;

        then (y | REAL ) is continuous by FDIFF_1: 25;

        then

         A59: (y | (f .: [.a, b.])) is continuous by FCONT_1: 16;

        ( rng f) c= ( dom y) by A55;

        then

         A60: ( dom (y * f)) = ( dom f) by RELAT_1: 27;

        

         A61: [.a, b.] c= ( dom f) by A1, A47, XBOOLE_1: 1;

        then

         A62: ].a, b.[ c= ( dom f) by A50, XBOOLE_1: 1;

        (( diff (f, ].a, b.[)) . 0 ) is_differentiable_on ].a, b.[ by A49;

        then (f | ].a, b.[) is_differentiable_on ].a, b.[ by Def5;

        then for x be Real st x in ].a, b.[ holds (f | ].a, b.[) is_differentiable_in x by FDIFF_1: 9;

        then

         A63: f is_differentiable_on ].a, b.[ by A62, FDIFF_1:def 6;

        

         A64: for x be Real st x in ].a, b.[ holds (y * f) is_differentiable_in x & ( diff ((y * f),x)) = ( - ((((( diff (f, ].a, b.[)) . ( 0 + 1)) . x) * ((a - x) |^ 0 )) / ( 0 ! )))

        proof

          

           A65: (( diff (f, ].a, b.[)) . ( 0 + 1)) = ((( diff (f, ].a, b.[)) . 0 ) `| ].a, b.[) by Def5

          .= ((f | ].a, b.[) `| ].a, b.[) by Def5

          .= (f `| ].a, b.[) by A63, FDIFF_2: 16;

          let x be Real such that

           A66: x in ].a, b.[;

          

           A67: f is_differentiable_in x by A63, A66, FDIFF_1: 9;

          

           A68: y is_differentiable_in (f . x) by A57;

          hence (y * f) is_differentiable_in x by A67, FDIFF_2: 13;

          

           A69: (((a - x) |^ 0 ) / ( 0 ! )) = 1 by NEWTON: 4, NEWTON: 12;

          

          thus ( diff ((y * f),x)) = (( diff (y,(f . x))) * ( diff (f,x))) by A68, A67, FDIFF_2: 13

          .= (( diff (y,(f . x))) * ((f `| ].a, b.[) . x)) by A63, A66, FDIFF_1:def 7

          .= (( - 1) * ((( diff (f, ].a, b.[)) . ( 0 + 1)) . x)) by A57, A65

          .= ( - (((( diff (f, ].a, b.[)) . ( 0 + 1)) . x) * (((a - x) |^ 0 ) / ( 0 ! )))) by A69

          .= ( - ((((( diff (f, ].a, b.[)) . ( 0 + 1)) . x) * ((a - x) |^ 0 )) / ( 0 ! ))) by XCMPLX_1: 74;

        end;

        then for x be Real st x in ].a, b.[ holds (y * f) is_differentiable_in x;

        then

         A70: (y * f) is_differentiable_on ].a, b.[ by A62, A60, FDIFF_1: 9;

        

         A71: ( dom ((y * f) | [.a, b.])) = (( dom (y * f)) /\ [.a, b.]) by RELAT_1: 61

        .= [.a, b.] by A1, A47, A58, XBOOLE_1: 1, XBOOLE_1: 28

        .= (Z /\ [.a, b.]) by A47, XBOOLE_1: 28

        .= ( dom (g | [.a, b.])) by A52, RELAT_1: 61;

         A72:

        now

          let xx be object such that

           A73: xx in ( dom (g | [.a, b.]));

          reconsider x = xx as Real by A73;

          ( dom (g | [.a, b.])) = (( dom g) /\ [.a, b.]) by RELAT_1: 61;

          then ( dom (g | [.a, b.])) c= [.a, b.] by XBOOLE_1: 17;

          then

           A74: x in [.a, b.] by A73;

          

          thus ((g | [.a, b.]) . xx) = (g . x) by A73, FUNCT_1: 47

          .= ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . 0 )) by A47, A53, A74

          .= ((f . a) - (( Taylor (f,Z,x,a)) . 0 )) by SERIES_1:def 1

          .= ((f . a) - ((((( diff (f,Z)) . 0 ) . x) * ((a - x) |^ 0 )) / ( 0 ! ))) by Def7

          .= ((f . a) - ((((f | Z) . x) * ((a - x) |^ 0 )) / ( 0 ! ))) by Def5

          .= ((f . a) - (((f . x) * ((a - x) |^ 0 )) / ( 0 ! ))) by A47, A74, FUNCT_1: 49

          .= ((f . a) - ((f . x) * 1)) by NEWTON: 4, NEWTON: 12

          .= (y . (f . x)) by A56

          .= ((y * f) . x) by A61, A74, FUNCT_1: 13

          .= (((y * f) | [.a, b.]) . xx) by A71, A73, FUNCT_1: 47;

        end;

        ((f | Z) | [.a, b.]) is continuous by A48, Def5;

        then (((f | Z) | [.a, b.]) | [.a, b.]) is continuous by FCONT_1: 15;

        then ((f | [.a, b.]) | [.a, b.]) is continuous by A47, FUNCT_1: 51;

        then (f | [.a, b.]) is continuous by FCONT_1: 15;

        then ((y * f) | [.a, b.]) is continuous by A59, FCONT_1: 25;

        hence (g | [.a, b.]) is continuous by A71, A72, FUNCT_1: 2;

        

         A75: ( dom ((y * f) | ].a, b.[)) = (( dom (y * f)) /\ ].a, b.[) by RELAT_1: 61

        .= ].a, b.[ by A50, A61, A60, XBOOLE_1: 1, XBOOLE_1: 28

        .= (Z /\ ].a, b.[) by A47, A50, XBOOLE_1: 1, XBOOLE_1: 28

        .= ( dom (g | ].a, b.[)) by A52, RELAT_1: 61;

        now

          let xx be object such that

           A76: xx in ( dom (g | ].a, b.[));

          reconsider x = xx as Real by A76;

          ( dom (g | ].a, b.[)) = (( dom g) /\ ].a, b.[) by RELAT_1: 61;

          then ( dom (g | ].a, b.[)) c= ].a, b.[ by XBOOLE_1: 17;

          then

           A77: x in ].a, b.[ by A76;

          

           A78: (((a - x) |^ 0 ) / ( 0 ! )) = 1 by NEWTON: 4, NEWTON: 12;

          

          thus ((g | ].a, b.[) . xx) = (g . x) by A76, FUNCT_1: 47

          .= ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . 0 )) by A53, A51, A77

          .= ((f . a) - (( Taylor (f,Z,x,a)) . 0 )) by SERIES_1:def 1

          .= ((f . a) - ((((( diff (f,Z)) . 0 ) . x) * ((a - x) |^ 0 )) / ( 0 ! ))) by Def7

          .= ((f . a) - ((((f | Z) . x) * ((a - x) |^ 0 )) / ( 0 ! ))) by Def5

          .= ((f . a) - (((f . x) * ((a - x) |^ 0 )) / ( 0 ! ))) by A51, A77, FUNCT_1: 49

          .= ((f . a) - ((f . x) * (((a - x) |^ 0 ) / ( 0 ! )))) by XCMPLX_1: 74

          .= (y . (f . x)) by A56, A78

          .= ((y * f) . x) by A62, A77, FUNCT_1: 13

          .= (((y * f) | ].a, b.[) . xx) by A75, A76, FUNCT_1: 47;

        end;

        then

         A79: (g | ].a, b.[) = ((y * f) | ].a, b.[) by A75, FUNCT_1: 2;

        then (g | ].a, b.[) is_differentiable_on ].a, b.[ by A70, FDIFF_2: 16;

        then for x be Real st x in ].a, b.[ holds (g | ].a, b.[) is_differentiable_in x by FDIFF_1: 9;

        hence

         A80: g is_differentiable_on ].a, b.[ by A52, A51, FDIFF_1:def 6;

        now

          let x be Real such that

           A81: x in ].a, b.[;

          thus g is_differentiable_in x by A80, A81, FDIFF_1: 9;

          

          thus ( diff (g,x)) = ((g `| ].a, b.[) . x) by A80, A81, FDIFF_1:def 7

          .= (((g | ].a, b.[) `| ].a, b.[) . x) by A80, FDIFF_2: 16

          .= (((y * f) `| ].a, b.[) . x) by A79, A70, FDIFF_2: 16

          .= ( diff ((y * f),x)) by A70, A81, FDIFF_1:def 7

          .= ( - ((((( diff (f, ].a, b.[)) . ( 0 + 1)) . x) * ((a - x) |^ 0 )) / ( 0 ! ))) by A64, A81;

        end;

        hence thesis;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A45, A2);

      hence thesis;

    end;

    

     Lm11: for n be Nat holds for f be PartFunc of REAL , REAL holds for Z be Subset of REAL st Z c= ( dom f) & f is_differentiable_on (n,Z) holds for a,b be Real st a < b & [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[) holds ex g be PartFunc of REAL , REAL st (( dom g) = Z & (for x be Real st x in Z holds (g . x) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . n))) & (g . a) = 0 & (g | [.a, b.]) is continuous & g is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (g,x)) = ( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n ! ))))

    proof

      let n be Nat;

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL such that

       A1: Z c= ( dom f) & f is_differentiable_on (n,Z);

      let a,b be Real such that

       A2: a < b & [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[);

      consider g be PartFunc of REAL , REAL such that

       A3: ( dom g) = Z & for x be Real st x in Z holds (g . x) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . n)) by Lm7;

      take g;

      thus thesis by A1, A2, A3, Lm10;

    end;

    theorem :: TAYLOR_1:28

    

     Th28: for n be Nat, f be PartFunc of REAL , REAL , Z be Subset of REAL st Z c= ( dom f) & f is_differentiable_on (n,Z) holds for a,b be Real st a < b & [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[) holds for l be Real, g be PartFunc of REAL , REAL st ( dom g) = ( [#] REAL ) & (for x be Real holds (g . x) = (((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) ! )))) & (((f . a) - (( Partial_Sums ( Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) ! ))) = 0 holds g is_differentiable_on ].a, b.[ & (g . b) = 0 & (g . a) = 0 & (g | [.a, b.]) is continuous & for x be Real st x in ].a, b.[ holds ( diff (g,x)) = (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n ! ))) + ((l * ((a - x) |^ n)) / (n ! )))

    proof

      let n be Nat;

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL such that

       A1: Z c= ( dom f) & f is_differentiable_on (n,Z);

      let a,b be Real such that

       A2: a < b and

       A3: [.a, b.] c= Z and

       A4: ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[);

      let l be Real;

      consider p be PartFunc of REAL , REAL such that

       A5: ( dom p) = ( [#] REAL ) and

       A6: for x be Real holds (p . x) = ((l * ((a - x) |^ (n + 1))) / ((n + 1) ! )) and

       A7: for x be Real holds p is_differentiable_in x & ( diff (p,x)) = ( - ((l * ((a - x) |^ n)) / (n ! ))) by Lm6;

      consider h be PartFunc of REAL , REAL such that

       A8: ( dom h) = Z and

       A9: for x be Real st x in Z holds (h . x) = ((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . n)) and

       A10: (h . a) = 0 and

       A11: (h | [.a, b.]) is continuous and

       A12: h is_differentiable_on ].a, b.[ and

       A13: for x be Real st x in ].a, b.[ holds ( diff (h,x)) = ( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n ! ))) by A1, A2, A3, A4, Lm11;

      

       A14: [.a, b.] c= (( dom h) /\ ( dom p)) by A3, A8, A5, XBOOLE_1: 19;

      let g be PartFunc of REAL , REAL such that

       A15: ( dom g) = ( [#] REAL ) and

       A16: for x be Real holds (g . x) = (((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) ! ))) and

       A17: (((f . a) - (( Partial_Sums ( Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) ! ))) = 0 ;

      set hp = (h - p);

      

       A18: ( dom hp) = (( dom h) /\ ( dom p)) by VALUED_1: 12

      .= Z by A8, A5, XBOOLE_1: 28;

      

       A19: for x be object st x in ( dom hp) holds (hp . x) = (g . x)

      proof

        let x be object such that

         A20: x in ( dom hp);

        reconsider xx = x as Real by A20;

        

        thus (hp . x) = ((h . xx) - (p . xx)) by A20, VALUED_1: 13

        .= (((f . a) - (( Partial_Sums ( Taylor (f,Z,xx,a))) . n)) - (p . xx)) by A9, A18, A20

        .= (((f . a) - (( Partial_Sums ( Taylor (f,Z,xx,a))) . n)) - ((l * ((a - xx) |^ (n + 1))) / ((n + 1) ! ))) by A6

        .= (g . x) by A16;

      end;

      for x be Real st x in REAL holds p is_differentiable_in x by A7;

      then p is_differentiable_on REAL by A5, FDIFF_1: 9;

      then (p | REAL ) is continuous by FDIFF_1: 25;

      then

       A21: (p | [.a, b.]) is continuous by FCONT_1: 16;

       ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

      then

       A22: ].a, b.[ c= Z by A3, XBOOLE_1: 1;

      

       A23: ( dom hp) = (( dom g) /\ Z) by A15, A18, XBOOLE_1: 28;

      

      then

       A24: (hp | ].a, b.[) = ((g | Z) | ].a, b.[) by A19, FUNCT_1: 46

      .= (g | ].a, b.[) by A22, FUNCT_1: 51;

      

       A25: for x be Real st x in ].a, b.[ holds hp is_differentiable_in x & ( diff (hp,x)) = (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n ! ))) + ((l * ((a - x) |^ n)) / (n ! )))

      proof

        let x be Real such that

         A26: x in ].a, b.[;

        

         A27: h is_differentiable_in x by A12, A26, FDIFF_1: 9;

        

         A28: p is_differentiable_in x by A7;

        hence hp is_differentiable_in x by A27, FDIFF_1: 14;

        

        thus ( diff (hp,x)) = (( diff (h,x)) - ( diff (p,x))) by A27, A28, FDIFF_1: 14

        .= (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n ! ))) - ( diff (p,x))) by A13, A26

        .= (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n ! ))) - ( - ((l * ((a - x) |^ n)) / (n ! )))) by A7

        .= (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n ! ))) + ((l * ((a - x) |^ n)) / (n ! )));

      end;

      then for x be Real st x in ].a, b.[ holds hp is_differentiable_in x;

      then

       A29: hp is_differentiable_on ].a, b.[ by A18, A22, FDIFF_1: 9;

      then for x be Real st x in ].a, b.[ holds (hp | ].a, b.[) is_differentiable_in x by FDIFF_1:def 6;

      hence

       A30: g is_differentiable_on ].a, b.[ by A15, A24, FDIFF_1:def 6;

      thus (g . b) = 0 by A16, A17;

      

       A31: a in [.a, b.] by A2, XXREAL_1: 1;

      

      then (g . a) = (hp . a) by A3, A18, A19

      .= ((h . a) - (p . a)) by A3, A18, A31, VALUED_1: 13

      .= ( 0 - ((l * ((a - a) |^ (n + 1))) / ((n + 1) ! ))) by A10, A6

      .= ( 0 - ((l * (( 0 |^ n) * 0 )) / ((n + 1) ! ))) by NEWTON: 6

      .= 0 ;

      hence (g . a) = 0 ;

      (hp | [.a, b.]) = ((g | Z) | [.a, b.]) by A23, A19, FUNCT_1: 46

      .= (g | [.a, b.]) by A3, FUNCT_1: 51;

      hence (g | [.a, b.]) is continuous by A11, A14, A21, FCONT_1: 18;

      thus for x be Real st x in ].a, b.[ holds ( diff (g,x)) = (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n ! ))) + ((l * ((a - x) |^ n)) / (n ! )))

      proof

        let x be Real such that

         A32: x in ].a, b.[;

        

        thus ( diff (g,x)) = ((g `| ].a, b.[) . x) by A30, A32, FDIFF_1:def 7

        .= (((g | ].a, b.[) `| ].a, b.[) . x) by A30, FDIFF_2: 16

        .= ((hp `| ].a, b.[) . x) by A24, A29, FDIFF_2: 16

        .= ( diff (hp,x)) by A29, A32, FDIFF_1:def 7

        .= (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n ! ))) + ((l * ((a - x) |^ n)) / (n ! ))) by A25, A32;

      end;

    end;

    theorem :: TAYLOR_1:29

    

     Th29: for n be Nat, f be PartFunc of REAL , REAL , Z be Subset of REAL st Z c= ( dom f) & f is_differentiable_on (n,Z) holds for a,b be Real st a < b & [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[) holds ex c be Real st c in ].a, b.[ & (f . a) = ((( Partial_Sums ( Taylor (f,Z,b,a))) . n) + ((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) ! )))

    proof

      let n be Nat;

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL such that

       A1: Z c= ( dom f) & f is_differentiable_on (n,Z);

      let a,b be Real such that

       A2: a < b and

       A3: [.a, b.] c= Z & ((( diff (f,Z)) . n) | [.a, b.]) is continuous & f is_differentiable_on ((n + 1), ].a, b.[);

      reconsider aa = a, bb = b as Real;

      (a - b) <> 0 by A2;

      then

       A4: ((a - b) |^ (n + 1)) <> 0 by CARD_4: 3;

      deffunc F( Real) = ( In (((f . a) - (( Partial_Sums ( Taylor (f,Z,$1,a))) . n)), REAL ));

      reconsider l = ( F(bb) / (((a - b) |^ (n + 1)) / ((n + 1) ! ))) as Real;

      consider g be Function of REAL , REAL such that

       A5: for x be Real holds (g . x) = (((f . a) - (( Partial_Sums ( Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) ! ))) by Th26;

      

       A6: (((f . a) - (( Partial_Sums ( Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) ! ))) = ( F(bb) - (( F(bb) / (((a - b) |^ (n + 1)) / ((n + 1) ! ))) * (((a - b) |^ (n + 1)) / ((n + 1) ! )))) by XCMPLX_1: 74

      .= ( F(bb) - F(bb)) by A4, XCMPLX_1: 50, XCMPLX_1: 87

      .= 0 ;

      then

       A7: (g . b) = 0 by A5;

      

       A8: ( dom g) = REAL by FUNCT_2:def 1;

      then

       A9: (g | [.a, b.]) is continuous by A1, A2, A3, A5, A6, Th28;

      g is_differentiable_on ].a, b.[ & (g . a) = 0 by A1, A2, A3, A5, A6, A8, Th28;

      then

      consider c be Real such that

       A10: c in ].a, b.[ and

       A11: ( diff (g,c)) = 0 by A2, A8, A7, A9, ROLLE: 1;

      c in { r where r be Real : a < r & r < b } by A10, RCOMP_1:def 2;

      then ex r be Real st c = r & a < r & r < b;

      then (a - c) <> 0 ;

      then

       A12: ((a - c) |^ n) <> 0 by CARD_4: 3;

      ( dom g) = REAL by FUNCT_2:def 1;

      then (( - ((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((a - c) |^ n)) / (n ! ))) + ((l * ((a - c) |^ n)) / (n ! ))) = 0 by A1, A2, A3, A5, A6, A10, A11, Th28;

      then ((((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((a - c) |^ n)) / (n ! )) * (n ! )) - (((l * ((a - c) |^ n)) / (n ! )) * (n ! ))) = 0 ;

      then ((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((a - c) |^ n)) - (((l * ((a - c) |^ n)) / (n ! )) * (n ! ))) = 0 by XCMPLX_1: 87;

      then (((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((a - c) |^ n)) - (l * ((a - c) |^ n))) / ((a - c) |^ n)) = ( 0 / ((a - c) |^ n)) by XCMPLX_1: 87;

      then (((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((a - c) |^ n)) / ((a - c) |^ n)) - ((l * ((a - c) |^ n)) / ((a - c) |^ n))) = 0 by XCMPLX_1: 120;

      then (((( diff (f, ].a, b.[)) . (n + 1)) . c) - ((l * ((a - c) |^ n)) / ((a - c) |^ n))) = 0 by A12, XCMPLX_1: 89;

      then ((( diff (f, ].a, b.[)) . (n + 1)) . c) = l by A12, XCMPLX_1: 89;

      then (f . a) = (((((( diff (f, ].a, b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) ! )) + (( Partial_Sums ( Taylor (f,Z,b,a))) . n)) by A6;

      hence thesis by A10;

    end;

    theorem :: TAYLOR_1:30

    

     Th30: for f be PartFunc of REAL , REAL , Z be Subset of REAL , Z1 be open Subset of REAL st Z1 c= Z holds for n be Nat st f is_differentiable_on (n,Z) holds ((( diff (f,Z)) . n) | Z1) = (( diff (f,Z1)) . n)

    proof

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL ;

      let Z1 be open Subset of REAL such that

       A1: Z1 c= Z;

      defpred P[ Nat] means f is_differentiable_on ($1,Z) implies ((( diff (f,Z)) . $1) | Z1) = (( diff (f,Z1)) . $1);

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A3: P[k];

        assume

         A4: f is_differentiable_on ((k + 1),Z);

        

         A5: (( diff (f,Z)) . k) is_differentiable_on Z by A4;

        then

         A6: (( diff (f,Z)) . k) is_differentiable_on Z1 by A1, FDIFF_1: 26;

        then

         A7: ( dom ((( diff (f,Z)) . k) `| Z1)) = Z1 by FDIFF_1:def 7;

        

         A8: ( dom (((( diff (f,Z)) . k) `| Z) | Z1)) = (( dom ((( diff (f,Z)) . k) `| Z)) /\ Z1) by RELAT_1: 61

        .= (Z /\ Z1) by A5, FDIFF_1:def 7

        .= Z1 by A1, XBOOLE_1: 28;

         A9:

        now

          let x be Element of REAL such that

           A10: x in ( dom (((( diff (f,Z)) . k) `| Z) | Z1));

          

          thus ((((( diff (f,Z)) . k) `| Z) | Z1) . x) = (((( diff (f,Z)) . k) `| Z) . x) by A8, A10, FUNCT_1: 49

          .= ( diff ((( diff (f,Z)) . k),x)) by A1, A5, A8, A10, FDIFF_1:def 7

          .= (((( diff (f,Z)) . k) `| Z1) . x) by A6, A8, A10, FDIFF_1:def 7;

        end;

        

        thus ((( diff (f,Z)) . (k + 1)) | Z1) = (((( diff (f,Z)) . k) `| Z) | Z1) by Def5

        .= ((( diff (f,Z)) . k) `| Z1) by A8, A7, A9, PARTFUN1: 5

        .= ((( diff (f,Z1)) . k) `| Z1) by A3, A4, A6, Th23, FDIFF_2: 16, NAT_1: 11

        .= (( diff (f,Z1)) . (k + 1)) by Def5;

      end;

      

       A11: P[ 0 ]

      proof

        assume f is_differentiable_on ( 0 ,Z);

        

        thus ((( diff (f,Z)) . 0 ) | Z1) = ((f | Z) | Z1) by Def5

        .= (f | Z1) by A1, FUNCT_1: 51

        .= (( diff (f,Z1)) . 0 ) by Def5;

      end;

      thus for k be Nat holds P[k] from NAT_1:sch 2( A11, A2);

    end;

    theorem :: TAYLOR_1:31

    

     Th31: for f be PartFunc of REAL , REAL , Z be Subset of REAL , Z1 be open Subset of REAL st Z1 c= Z holds for n be Nat st f is_differentiable_on ((n + 1),Z) holds f is_differentiable_on ((n + 1),Z1)

    proof

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL ;

      let Z1 be open Subset of REAL such that

       A1: Z1 c= Z;

      let n be Nat such that

       A2: f is_differentiable_on ((n + 1),Z);

      now

        let k be Nat such that

         A3: k <= ((n + 1) - 1);

        (( diff (f,Z)) . k) is_differentiable_on Z by A2, A3;

        then (( diff (f,Z)) . k) is_differentiable_on Z1 by A1, FDIFF_1: 26;

        then

         A4: ((( diff (f,Z)) . k) | Z1) is_differentiable_on Z1 by FDIFF_2: 16;

        n <= (n + 1) by NAT_1: 11;

        then k <= (n + 1) by A3, XXREAL_0: 2;

        hence (( diff (f,Z1)) . k) is_differentiable_on Z1 by A1, A2, A4, Th23, Th30;

      end;

      hence thesis;

    end;

    theorem :: TAYLOR_1:32

    

     Th32: for f be PartFunc of REAL , REAL , Z be Subset of REAL , x be Real st x in Z holds for n be Nat holds (f . x) = (( Partial_Sums ( Taylor (f,Z,x,x))) . n)

    proof

      let f be PartFunc of REAL , REAL ;

      let Z be Subset of REAL ;

      let x be Real such that

       A1: x in Z;

      defpred P[ Nat] means (f . x) = (( Partial_Sums ( Taylor (f,Z,x,x))) . $1);

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A3: P[k];

        

        thus (( Partial_Sums ( Taylor (f,Z,x,x))) . (k + 1)) = ((( Partial_Sums ( Taylor (f,Z,x,x))) . k) + (( Taylor (f,Z,x,x)) . (k + 1))) by SERIES_1:def 1

        .= ((f . x) + ((((( diff (f,Z)) . (k + 1)) . x) * ((x - x) |^ (k + 1))) / ((k + 1) ! ))) by A3, Def7

        .= ((f . x) + ((((( diff (f,Z)) . (k + 1)) . x) * (( 0 |^ k) * 0 )) / ((k + 1) ! ))) by NEWTON: 6

        .= (f . x);

      end;

      (( Partial_Sums ( Taylor (f,Z,x,x))) . 0 ) = (( Taylor (f,Z,x,x)) . 0 ) by SERIES_1:def 1

      .= ((((( diff (f,Z)) . 0 ) . x) * ((x - x) |^ 0 )) / ( 0 ! )) by Def7

      .= ((((f | Z) . x) * ((x - x) |^ 0 )) / ( 0 ! )) by Def5

      .= ((((f | Z) . x) * 1) / 1) by NEWTON: 4, NEWTON: 12

      .= (f . x) by A1, FUNCT_1: 49;

      then

       A4: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: TAYLOR_1:33

    for n be Nat, f be PartFunc of REAL , REAL , x0,r be Real st ].(x0 - r), (x0 + r).[ c= ( dom f) & 0 < r & f is_differentiable_on ((n + 1), ].(x0 - r), (x0 + r).[) holds for x be Real st x in ].(x0 - r), (x0 + r).[ holds ex s be Real st 0 < s & s < 1 & (f . x) = ((( Partial_Sums ( Taylor (f, ].(x0 - r), (x0 + r).[,x0,x))) . n) + ((((( diff (f, ].(x0 - r), (x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! )))

    proof

      let n be Nat;

      let f be PartFunc of REAL , REAL ;

      let x0,r be Real such that

       A1: ].(x0 - r), (x0 + r).[ c= ( dom f) and

       A2: 0 < r and

       A3: f is_differentiable_on ((n + 1), ].(x0 - r), (x0 + r).[);

      let x be Real such that

       A4: x in ].(x0 - r), (x0 + r).[;

      now

        per cases by XXREAL_0: 1;

          case

           A5: x < x0;

           |.(x0 - x0).| = 0 by ABSVALUE: 2;

          then x0 in ].(x0 - r), (x0 + r).[ by A2, RCOMP_1: 1;

          then

           A6: [.x, x0.] c= ].(x0 - r), (x0 + r).[ by A4, XXREAL_2:def 12;

          (( diff (f, ].(x0 - r), (x0 + r).[)) . n) is_differentiable_on ].(x0 - r), (x0 + r).[ by A3;

          then ((( diff (f, ].(x0 - r), (x0 + r).[)) . n) | ].(x0 - r), (x0 + r).[) is continuous by FDIFF_1: 25;

          then

           A7: ((( diff (f, ].(x0 - r), (x0 + r).[)) . n) | [.x, x0.]) is continuous by A6, FCONT_1: 16;

          

           A8: f is_differentiable_on (n, ].(x0 - r), (x0 + r).[) by A3, Th23, NAT_1: 11;

          set t = (x0 - x);

          

           A9: t > 0 by A5, XREAL_1: 50;

          

           A10: ].x, x0.[ c= [.x, x0.] by XXREAL_1: 25;

          then f is_differentiable_on ((n + 1), ].x, x0.[) by A3, A6, Th31, XBOOLE_1: 1;

          then

          consider c be Real such that

           A11: c in ].x, x0.[ and

           A12: (f . x) = ((( Partial_Sums ( Taylor (f, ].(x0 - r), (x0 + r).[,x0,x))) . n) + ((((( diff (f, ].x, x0.[)) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) ! ))) by A1, A5, A6, A8, A7, Th29;

          take s = ((x0 - c) / t);

          

           A13: (x0 + (s * (x - x0))) = (x0 - (((x0 - c) / t) * t))

          .= (x0 - (x0 - c)) by A9, XCMPLX_1: 87

          .= c;

          c in { p where p be Real : (x0 - t) < p & p < x0 } by A11, RCOMP_1:def 2;

          then

           A14: ex g be Real st g = c & (x0 - t) < g & g < x0;

          then 0 < (x0 - c) by XREAL_1: 50;

          then ( 0 / t) < ((x0 - c) / t) by A9, XREAL_1: 74;

          hence 0 < s;

          ((x0 - t) + t) < (c + t) by A14, XREAL_1: 8;

          then (x0 - c) < t by XREAL_1: 19;

          then ((x0 - c) / t) < (t / t) by A9, XREAL_1: 74;

          hence s < 1 by A9, XCMPLX_1: 60;

          ((( diff (f, ].x, x0.[)) . (n + 1)) . c) = (((( diff (f, ].(x0 - r), (x0 + r).[)) . (n + 1)) | ].x, x0.[) . c) by A3, A6, A10, Th30, XBOOLE_1: 1

          .= ((( diff (f, ].(x0 - r), (x0 + r).[)) . (n + 1)) . c) by A11, FUNCT_1: 49;

          hence (f . x) = ((( Partial_Sums ( Taylor (f, ].(x0 - r), (x0 + r).[,x0,x))) . n) + ((((( diff (f, ].(x0 - r), (x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! ))) by A12, A13;

        end;

          case

           A15: x = x0;

          set s = (1 / 2);

          take s;

          thus 0 < s & s < 1;

          set c = (x0 + (s * (x - x0)));

          

          thus ((( Partial_Sums ( Taylor (f, ].(x0 - r), (x0 + r).[,x0,x))) . n) + ((((( diff (f, ].(x0 - r), (x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! ))) = ((f . x) + ((((( diff (f, ].(x0 - r), (x0 + r).[)) . (n + 1)) . c) * ((x - x) |^ (n + 1))) / ((n + 1) ! ))) by A4, A15, Th32

          .= ((f . x) + ((((( diff (f, ].(x0 - r), (x0 + r).[)) . (n + 1)) . c) * (( 0 |^ n) * 0 )) / ((n + 1) ! ))) by NEWTON: 6

          .= (f . x);

        end;

          case

           A16: x > x0;

          set t = (x - x0);

          

           A17: f is_differentiable_on (n, ].(x0 - r), (x0 + r).[) by A3, Th23, NAT_1: 11;

           |.(x0 - x0).| = 0 by ABSVALUE: 2;

          then x0 in ].(x0 - r), (x0 + r).[ by A2, RCOMP_1: 1;

          then

           A18: [.x0, x.] c= ].(x0 - r), (x0 + r).[ by A4, XXREAL_2:def 12;

          (( diff (f, ].(x0 - r), (x0 + r).[)) . n) is_differentiable_on ].(x0 - r), (x0 + r).[ by A3;

          then ((( diff (f, ].(x0 - r), (x0 + r).[)) . n) | ].(x0 - r), (x0 + r).[) is continuous by FDIFF_1: 25;

          then

           A19: ((( diff (f, ].(x0 - r), (x0 + r).[)) . n) | [.x0, x.]) is continuous by A18, FCONT_1: 16;

          

           A20: ].x0, x.[ c= [.x0, x.] by XXREAL_1: 25;

          then f is_differentiable_on ((n + 1), ].x0, x.[) by A3, A18, Th31, XBOOLE_1: 1;

          then

          consider c be Real such that

           A21: c in ].x0, x.[ and

           A22: (f . x) = ((( Partial_Sums ( Taylor (f, ].(x0 - r), (x0 + r).[,x0,x))) . n) + ((((( diff (f, ].x0, x.[)) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) ! ))) by A1, A16, A18, A17, A19, Th27;

          take s = ((c - x0) / t);

          

           A23: t > 0 by A16, XREAL_1: 50;

          

          then

           A24: (x0 + (s * (x - x0))) = (x0 + (c - x0)) by XCMPLX_1: 87

          .= c;

          c in { p where p be Real : x0 < p & p < (x0 + t) } by A21, RCOMP_1:def 2;

          then

           A25: ex g be Real st g = c & x0 < g & g < (x0 + t);

          then 0 < (c - x0) by XREAL_1: 50;

          then ( 0 / t) < ((c - x0) / t) by A23, XREAL_1: 74;

          hence 0 < s;

          (c - x0) < t by A25, XREAL_1: 19;

          then ((c - x0) / t) < (t / t) by A23, XREAL_1: 74;

          hence s < 1 by A23, XCMPLX_1: 60;

          ((( diff (f, ].x0, x.[)) . (n + 1)) . c) = (((( diff (f, ].(x0 - r), (x0 + r).[)) . (n + 1)) | ].x0, x.[) . c) by A3, A18, A20, Th30, XBOOLE_1: 1

          .= ((( diff (f, ].(x0 - r), (x0 + r).[)) . (n + 1)) . c) by A21, FUNCT_1: 49;

          hence (f . x) = ((( Partial_Sums ( Taylor (f, ].(x0 - r), (x0 + r).[,x0,x))) . n) + ((((( diff (f, ].(x0 - r), (x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! ))) by A22, A24;

        end;

      end;

      hence thesis;

    end;