diff_3.miz



    begin

    reserve n,m for Element of NAT ;

    reserve h,k,r,r1,r2,x,x0,x1,x2,x3 for Real;

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

    theorem :: DIFF_3:1

    

     Th1: (( cD (f,h)) . x) = ((( fD (f,(h / 2))) . x) - (( fD (f,( - (h / 2)))) . x))

    proof

      (( cD (f,h)) . x) = ((((f . (x + (h / 2))) - (f . x)) + (f . x)) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= (((f . (x + (h / 2))) - (f . x)) - ((f . (x - (h / 2))) - (f . x)))

      .= ((( fD (f,(h / 2))) . x) - ((f . (x - (h / 2))) - (f . x))) by DIFF_1: 3

      .= ((( fD (f,(h / 2))) . x) - (( fD (f,( - (h / 2)))) . x)) by DIFF_1: 3;

      hence thesis;

    end;

    theorem :: DIFF_3:2

    

     Th2: (( fD (f,( - (h / 2)))) . x) = ( - (( bD (f,(h / 2))) . x))

    proof

      (( fD (f,( - (h / 2)))) . x) = ((f . (x - (h / 2))) - (f . x)) by DIFF_1: 3

      .= ( - ((f . x) - (f . (x - (h / 2)))))

      .= ( - (( bD (f,(h / 2))) . x)) by DIFF_1: 4;

      hence thesis;

    end;

    theorem :: DIFF_3:3

    (( cD (f,h)) . x) = ((( bD (f,(h / 2))) . x) - (( bD (f,( - (h / 2)))) . x))

    proof

      (( fD (f,(h / 2))) . x) = ( - (( bD (f,( - (h / 2)))) . x))

      proof

        (( fD (f,(h / 2))) . x) = ((f . (x + (h / 2))) - (f . x)) by DIFF_1: 3

        .= ( - ((f . x) - (f . (x - ( - (h / 2))))))

        .= ( - (( bD (f,( - (h / 2)))) . x)) by DIFF_1: 4;

        hence thesis;

      end;

      

      then (( cD (f,h)) . x) = (( - (( bD (f,( - (h / 2)))) . x)) - (( fD (f,( - (h / 2)))) . x)) by Th1

      .= (( - (( bD (f,( - (h / 2)))) . x)) - ( - (( bD (f,(h / 2))) . x))) by Th2

      .= ((( bD (f,(h / 2))) . x) - (( bD (f,( - (h / 2)))) . x));

      hence thesis;

    end;

    theorem :: DIFF_3:4

    ((( fdif (((r (#) f1) + f2),h)) . (n + 1)) . x) = ((r * ((( fdif (f1,h)) . (n + 1)) . x)) + ((( fdif (f2,h)) . (n + 1)) . x))

    proof

      set g = (r (#) f1);

      ((( fdif (((r (#) f1) + f2),h)) . (n + 1)) . x) = (((( fdif (g,h)) . (n + 1)) . x) + ((( fdif (f2,h)) . (n + 1)) . x)) by DIFF_1: 8

      .= ((r * ((( fdif (f1,h)) . (n + 1)) . x)) + ((( fdif (f2,h)) . (n + 1)) . x)) by DIFF_1: 7;

      hence thesis;

    end;

    theorem :: DIFF_3:5

    ((( fdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x) = (((( fdif (f1,h)) . (n + 1)) . x) + (r * ((( fdif (f2,h)) . (n + 1)) . x)))

    proof

      set g = (r (#) f2);

      ((( fdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x) = (((( fdif (f1,h)) . (n + 1)) . x) + ((( fdif (g,h)) . (n + 1)) . x)) by DIFF_1: 8

      .= (((( fdif (f1,h)) . (n + 1)) . x) + (r * ((( fdif (f2,h)) . (n + 1)) . x))) by DIFF_1: 7;

      hence thesis;

    end;

    theorem :: DIFF_3:6

    ((( fdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x) = ((r1 * ((( fdif (f1,h)) . (n + 1)) . x)) - (r2 * ((( fdif (f2,h)) . (n + 1)) . x)))

    proof

      set g1 = (r1 (#) f1);

      set g2 = (r2 (#) f2);

      ((( fdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x) = (((( fdif (g1,h)) . (n + 1)) . x) - ((( fdif (g2,h)) . (n + 1)) . x)) by DIFF_1: 9

      .= ((r1 * ((( fdif (f1,h)) . (n + 1)) . x)) - ((( fdif (g2,h)) . (n + 1)) . x)) by DIFF_1: 7

      .= ((r1 * ((( fdif (f1,h)) . (n + 1)) . x)) - (r2 * ((( fdif (f2,h)) . (n + 1)) . x))) by DIFF_1: 7;

      hence thesis;

    end;

    theorem :: DIFF_3:7

    (( fdif (f,h)) . 1) = ( fD (f,h))

    proof

      (( fdif (f,h)) . 1) = (( fdif (f,h)) . ( 0 + 1))

      .= ( fD ((( fdif (f,h)) . 0 ),h)) by DIFF_1:def 6

      .= ( fD (f,h)) by DIFF_1:def 6;

      hence thesis;

    end;

    theorem :: DIFF_3:8

    ((( bdif (((r (#) f1) + f2),h)) . (n + 1)) . x) = ((r * ((( bdif (f1,h)) . (n + 1)) . x)) + ((( bdif (f2,h)) . (n + 1)) . x))

    proof

      set g = (r (#) f1);

      ((( bdif (((r (#) f1) + f2),h)) . (n + 1)) . x) = (((( bdif (g,h)) . (n + 1)) . x) + ((( bdif (f2,h)) . (n + 1)) . x)) by DIFF_1: 15

      .= ((r * ((( bdif (f1,h)) . (n + 1)) . x)) + ((( bdif (f2,h)) . (n + 1)) . x)) by DIFF_1: 14;

      hence thesis;

    end;

    theorem :: DIFF_3:9

    ((( bdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x) = (((( bdif (f1,h)) . (n + 1)) . x) + (r * ((( bdif (f2,h)) . (n + 1)) . x)))

    proof

      set g = (r (#) f2);

      ((( bdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x) = (((( bdif (f1,h)) . (n + 1)) . x) + ((( bdif (g,h)) . (n + 1)) . x)) by DIFF_1: 15

      .= (((( bdif (f1,h)) . (n + 1)) . x) + (r * ((( bdif (f2,h)) . (n + 1)) . x))) by DIFF_1: 14;

      hence thesis;

    end;

    theorem :: DIFF_3:10

    ((( bdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x) = ((r1 * ((( bdif (f1,h)) . (n + 1)) . x)) - (r2 * ((( bdif (f2,h)) . (n + 1)) . x)))

    proof

      set g1 = (r1 (#) f1);

      set g2 = (r2 (#) f2);

      ((( bdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x) = (((( bdif (g1,h)) . (n + 1)) . x) - ((( bdif (g2,h)) . (n + 1)) . x)) by DIFF_1: 16

      .= ((r1 * ((( bdif (f1,h)) . (n + 1)) . x)) - ((( bdif (g2,h)) . (n + 1)) . x)) by DIFF_1: 14

      .= ((r1 * ((( bdif (f1,h)) . (n + 1)) . x)) - (r2 * ((( bdif (f2,h)) . (n + 1)) . x))) by DIFF_1: 14;

      hence thesis;

    end;

    theorem :: DIFF_3:11

    

     Th11: (( bdif (f,h)) . 1) = ( bD (f,h))

    proof

      (( bdif (f,h)) . 1) = (( bdif (f,h)) . ( 0 + 1))

      .= ( bD ((( bdif (f,h)) . 0 ),h)) by DIFF_1:def 7

      .= ( bD (f,h)) by DIFF_1:def 7;

      hence thesis;

    end;

    theorem :: DIFF_3:12

    ((( bdif ((( bdif (f,h)) . m),h)) . n) . x) = ((( bdif (f,h)) . (m + n)) . x)

    proof

      defpred X[ Nat] means for x holds ((( bdif ((( bdif (f,h)) . m),h)) . $1) . x) = ((( bdif (f,h)) . (m + $1)) . x);

      

       A1: X[ 0 ] by DIFF_1:def 7;

      

       A2: for i be Nat st X[i] holds X[(i + 1)]

      proof

        let i be Nat;

        assume

         A3: for x holds ((( bdif ((( bdif (f,h)) . m),h)) . i) . x) = ((( bdif (f,h)) . (m + i)) . x);

        let x;

        (( bdif (f,h)) . m) is Function of REAL , REAL by DIFF_1: 12;

        then

         A4: (( bdif ((( bdif (f,h)) . m),h)) . i) is Function of REAL , REAL by DIFF_1: 12;

        

         A5: (( bdif (f,h)) . (m + i)) is Function of REAL , REAL by DIFF_1: 12;

        ((( bdif ((( bdif (f,h)) . m),h)) . (i + 1)) . x) = (( bD ((( bdif ((( bdif (f,h)) . m),h)) . i),h)) . x) by DIFF_1:def 7

        .= (((( bdif ((( bdif (f,h)) . m),h)) . i) . x) - ((( bdif ((( bdif (f,h)) . m),h)) . i) . (x - h))) by A4, DIFF_1: 4

        .= (((( bdif (f,h)) . (m + i)) . x) - ((( bdif ((( bdif (f,h)) . m),h)) . i) . (x - h))) by A3

        .= (((( bdif (f,h)) . (m + i)) . x) - ((( bdif (f,h)) . (m + i)) . (x - h))) by A3

        .= (( bD ((( bdif (f,h)) . (m + i)),h)) . x) by A5, DIFF_1: 4

        .= ((( bdif (f,h)) . ((m + i) + 1)) . x) by DIFF_1:def 7;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: DIFF_3:13

    ((( cdif (((r (#) f1) + f2),h)) . (n + 1)) . x) = ((r * ((( cdif (f1,h)) . (n + 1)) . x)) + ((( cdif (f2,h)) . (n + 1)) . x))

    proof

      set g = (r (#) f1);

      ((( cdif (((r (#) f1) + f2),h)) . (n + 1)) . x) = (((( cdif (g,h)) . (n + 1)) . x) + ((( cdif (f2,h)) . (n + 1)) . x)) by DIFF_1: 22

      .= ((r * ((( cdif (f1,h)) . (n + 1)) . x)) + ((( cdif (f2,h)) . (n + 1)) . x)) by DIFF_1: 21;

      hence thesis;

    end;

    theorem :: DIFF_3:14

    ((( cdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x) = (((( cdif (f1,h)) . (n + 1)) . x) + (r * ((( cdif (f2,h)) . (n + 1)) . x)))

    proof

      set g = (r (#) f2);

      ((( cdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x) = (((( cdif (f1,h)) . (n + 1)) . x) + ((( cdif (g,h)) . (n + 1)) . x)) by DIFF_1: 22

      .= (((( cdif (f1,h)) . (n + 1)) . x) + (r * ((( cdif (f2,h)) . (n + 1)) . x))) by DIFF_1: 21;

      hence thesis;

    end;

    theorem :: DIFF_3:15

    ((( cdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x) = ((r1 * ((( cdif (f1,h)) . (n + 1)) . x)) - (r2 * ((( cdif (f2,h)) . (n + 1)) . x)))

    proof

      set g1 = (r1 (#) f1);

      set g2 = (r2 (#) f2);

      ((( cdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x) = (((( cdif (g1,h)) . (n + 1)) . x) - ((( cdif (g2,h)) . (n + 1)) . x)) by DIFF_1: 23

      .= ((r1 * ((( cdif (f1,h)) . (n + 1)) . x)) - ((( cdif (g2,h)) . (n + 1)) . x)) by DIFF_1: 21

      .= ((r1 * ((( cdif (f1,h)) . (n + 1)) . x)) - (r2 * ((( cdif (f2,h)) . (n + 1)) . x))) by DIFF_1: 21;

      hence thesis;

    end;

    theorem :: DIFF_3:16

    

     Th16: (( cdif (f,h)) . 1) = ( cD (f,h))

    proof

      (( cdif (f,h)) . 1) = (( cdif (f,h)) . ( 0 + 1))

      .= ( cD ((( cdif (f,h)) . 0 ),h)) by DIFF_1:def 8

      .= ( cD (f,h)) by DIFF_1:def 8;

      hence thesis;

    end;

    theorem :: DIFF_3:17

    ((( cdif ((( cdif (f,h)) . m),h)) . n) . x) = ((( cdif (f,h)) . (m + n)) . x)

    proof

      defpred X[ Nat] means for x holds ((( cdif ((( cdif (f,h)) . m),h)) . $1) . x) = ((( cdif (f,h)) . (m + $1)) . x);

      

       A1: X[ 0 ] by DIFF_1:def 8;

      

       A2: for i be Nat st X[i] holds X[(i + 1)]

      proof

        let i be Nat;

        assume

         A3: for x holds ((( cdif ((( cdif (f,h)) . m),h)) . i) . x) = ((( cdif (f,h)) . (m + i)) . x);

        let x;

        (( cdif (f,h)) . m) is Function of REAL , REAL by DIFF_1: 19;

        then

         A4: (( cdif ((( cdif (f,h)) . m),h)) . i) is Function of REAL , REAL by DIFF_1: 19;

        

         A5: (( cdif (f,h)) . (m + i)) is Function of REAL , REAL by DIFF_1: 19;

        ((( cdif ((( cdif (f,h)) . m),h)) . (i + 1)) . x) = (( cD ((( cdif ((( cdif (f,h)) . m),h)) . i),h)) . x) by DIFF_1:def 8

        .= (((( cdif ((( cdif (f,h)) . m),h)) . i) . (x + (h / 2))) - ((( cdif ((( cdif (f,h)) . m),h)) . i) . (x - (h / 2)))) by A4, DIFF_1: 5

        .= (((( cdif (f,h)) . (m + i)) . (x + (h / 2))) - ((( cdif ((( cdif (f,h)) . m),h)) . i) . (x - (h / 2)))) by A3

        .= (((( cdif (f,h)) . (m + i)) . (x + (h / 2))) - ((( cdif (f,h)) . (m + i)) . (x - (h / 2)))) by A3

        .= (( cD ((( cdif (f,h)) . (m + i)),h)) . x) by A5, DIFF_1: 5

        .= ((( cdif (f,h)) . ((m + i) + 1)) . x) by DIFF_1:def 8;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: DIFF_3:18

    ((( fdif (f,h)) . n) . x) = ((( cdif (f,h)) . n) . (x + ((n / 2) * h))) implies ((( bdif (f,h)) . n) . x) = ((( cdif (f,h)) . n) . (x - ((n / 2) * h)))

    proof

      defpred X[ Nat] means for x holds ((( bdif (f,h)) . $1) . x) = ((( cdif (f,h)) . $1) . (x - (($1 / 2) * h)));

      

       A1: X[ 0 ]

      proof

        let x;

        ((( bdif (f,h)) . 0 ) . x) = (f . x) by DIFF_1:def 7

        .= ((( cdif (f,h)) . 0 ) . (x - (( 0 / 2) * h))) by DIFF_1:def 8;

        hence thesis;

      end;

      

       A2: for i be Nat st X[i] holds X[(i + 1)]

      proof

        let i be Nat;

        assume

         A3: for x holds ((( bdif (f,h)) . i) . x) = ((( cdif (f,h)) . i) . (x - ((i / 2) * h)));

        let x;

        

         A4: (( bdif (f,h)) . i) is Function of REAL , REAL by DIFF_1: 12;

        

         A5: (( cdif (f,h)) . i) is Function of REAL , REAL by DIFF_1: 19;

        ((( bdif (f,h)) . (i + 1)) . x) = (( bD ((( bdif (f,h)) . i),h)) . x) by DIFF_1:def 7

        .= (((( bdif (f,h)) . i) . x) - ((( bdif (f,h)) . i) . (x - h))) by A4, DIFF_1: 4

        .= (((( cdif (f,h)) . i) . (x - ((i / 2) * h))) - ((( bdif (f,h)) . i) . (x - h))) by A3

        .= (((( cdif (f,h)) . i) . (x - ((i / 2) * h))) - ((( cdif (f,h)) . i) . ((x - h) - ((i / 2) * h)))) by A3

        .= (((( cdif (f,h)) . i) . ((x - (((i + 1) / 2) * h)) + (h / 2))) - ((( cdif (f,h)) . i) . ((x - (((i + 1) / 2) * h)) - (h / 2))))

        .= (( cD ((( cdif (f,h)) . i),h)) . (x - (((i + 1) / 2) * h))) by A5, DIFF_1: 5

        .= ((( cdif (f,h)) . (i + 1)) . (x - (((i + 1) / 2) * h))) by DIFF_1:def 8;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: DIFF_3:19

    ((( fdif (f,h)) . n) . x) = ((( cdif (f,h)) . n) . ((x + (((n - 1) / 2) * h)) + (h / 2))) implies ((( bdif (f,h)) . n) . x) = ((( cdif (f,h)) . n) . ((x - (((n - 1) / 2) * h)) - (h / 2)))

    proof

      defpred X[ Nat] means for x holds ((( bdif (f,h)) . $1) . x) = ((( cdif (f,h)) . $1) . ((x - ((($1 - 1) / 2) * h)) - (h / 2)));

      

       A1: X[ 0 ]

      proof

        let x;

        ((( bdif (f,h)) . 0 ) . x) = (f . x) by DIFF_1:def 7

        .= ((( cdif (f,h)) . 0 ) . ((x - ((( 0 - 1) / 2) * h)) - (h / 2))) by DIFF_1:def 8;

        hence thesis;

      end;

      

       A2: for i be Nat st X[i] holds X[(i + 1)]

      proof

        let i be Nat;

        assume

         A3: for x holds ((( bdif (f,h)) . i) . x) = ((( cdif (f,h)) . i) . ((x - (((i - 1) / 2) * h)) - (h / 2)));

        let x;

        

         A4: (( bdif (f,h)) . i) is Function of REAL , REAL by DIFF_1: 12;

        

         A5: (( cdif (f,h)) . i) is Function of REAL , REAL by DIFF_1: 19;

        ((( bdif (f,h)) . (i + 1)) . x) = (( bD ((( bdif (f,h)) . i),h)) . x) by DIFF_1:def 7

        .= (((( bdif (f,h)) . i) . x) - ((( bdif (f,h)) . i) . (x - h))) by A4, DIFF_1: 4

        .= (((( cdif (f,h)) . i) . ((x - (((i - 1) / 2) * h)) - (h / 2))) - ((( bdif (f,h)) . i) . (x - h))) by A3

        .= (((( cdif (f,h)) . i) . ((x - (((i - 1) / 2) * h)) - (h / 2))) - ((( cdif (f,h)) . i) . (((x - h) - (((i - 1) / 2) * h)) - (h / 2)))) by A3

        .= (((( cdif (f,h)) . i) . (((x - ((i / 2) * h)) - (h / 2)) + (h / 2))) - ((( cdif (f,h)) . i) . (((x - ((i / 2) * h)) - (h / 2)) - (h / 2))))

        .= (( cD ((( cdif (f,h)) . i),h)) . ((x - ((i / 2) * h)) - (h / 2))) by A5, DIFF_1: 5

        .= ((( cdif (f,h)) . (i + 1)) . ((x - ((i / 2) * h)) - (h / 2))) by DIFF_1:def 8;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: DIFF_3:20

     [!f, x, (x + h)!] = ((( fD (f,h)) . x) / h)

    proof

       [!f, x, (x + h)!] = (( - ((f . (x + h)) - (f . x))) / ( - h))

      .= (((f . (x + h)) - (f . x)) / h) by XCMPLX_1: 191

      .= ((( fD (f,h)) . x) / h) by DIFF_1: 3;

      hence thesis;

    end;

    theorem :: DIFF_3:21

     [!f, (x - h), x!] = ((( bD (f,h)) . x) / h)

    proof

       [!f, (x - h), x!] = (((( bdif (f,h)) . 1) . x) / h) by DIFF_2: 3

      .= ((( bD (f,h)) . x) / h) by Th11;

      hence thesis;

    end;

    theorem :: DIFF_3:22

    

     Th22: [!f, (x - (h / 2)), (x + (h / 2))!] = ((( cD (f,h)) . x) / h)

    proof

       [!f, (x - (h / 2)), (x + (h / 2))!] = [!f, (x + (h / 2)), (x - (h / 2))!] by DIFF_1: 29

      .= ((( cD (f,h)) . x) / h) by DIFF_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_3:23

    

     Th23: [!f, (x - (h / 2)), (x + (h / 2))!] = (((( cdif (f,h)) . 1) . x) / h)

    proof

       [!f, (x - (h / 2)), (x + (h / 2))!] = ((( cD (f,h)) . x) / h) by Th22

      .= (((( cdif (f,h)) . 1) . x) / h) by Th16;

      hence thesis;

    end;

    theorem :: DIFF_3:24

    h <> 0 implies [!f, (x - h), x, (x + h)!] = (((( cdif (f,h)) . 2) . x) / ((2 * h) * h))

    proof

      assume h <> 0 ;

      then (x - h) <> x & (x - h) <> (x + h) & x <> (x + h);

      then

       A1: ((x - h),x,(x + h)) are_mutually_distinct by ZFMISC_1:def 5;

      

       A2: (( cdif (f,h)) . 1) is Function of REAL , REAL by DIFF_1: 19;

       [!f, (x - h), x, (x + h)!] = [!f, (x + h), x, (x - h)!] by A1, DIFF_1: 34

      .= (( [!f, x, (x + h)!] - [!f, x, (x - h)!]) / ((x + h) - (x - h))) by DIFF_1: 29

      .= (( [!f, ((x + (h / 2)) - (h / 2)), ((x + (h / 2)) + (h / 2))!] - [!f, ((x - (h / 2)) - (h / 2)), ((x - (h / 2)) + (h / 2))!]) / ((x + h) - (x - h))) by DIFF_1: 29

      .= (((((( cdif (f,h)) . 1) . (x + (h / 2))) / h) - [!f, ((x - (h / 2)) - (h / 2)), ((x - (h / 2)) + (h / 2))!]) / ((x + h) - (x - h))) by Th23

      .= (((((( cdif (f,h)) . 1) . (x + (h / 2))) / h) - (((( cdif (f,h)) . 1) . (x - (h / 2))) / h)) / ((x + h) - (x - h))) by Th23

      .= (((((( cdif (f,h)) . 1) . (x + (h / 2))) - ((( cdif (f,h)) . 1) . (x - (h / 2)))) / h) / ((x + h) - (x - h)))

      .= (((( cD ((( cdif (f,h)) . 1),h)) . x) / h) / (2 * h)) by A2, DIFF_1: 5

      .= ((((( cdif (f,h)) . (1 + 1)) . x) / h) / (2 * h)) by DIFF_1:def 8

      .= (((( cdif (f,h)) . 2) . x) / ((2 * h) * h)) by XCMPLX_1: 78;

      hence thesis;

    end;

    theorem :: DIFF_3:25

    

     Th25: [!(f1 - f2), x0, x1!] = ( [!f1, x0, x1!] - [!f2, x0, x1!])

    proof

      reconsider x0, x1 as Element of REAL by XREAL_0:def 1;

       [!(f1 - f2), x0, x1!] = ((((f1 . x0) - (f2 . x0)) - ((f1 - f2) . x1)) / (x0 - x1)) by VALUED_1: 15

      .= ((((f1 . x0) - (f2 . x0)) - ((f1 . x1) - (f2 . x1))) / (x0 - x1)) by VALUED_1: 15

      .= ( [!f1, x0, x1!] - [!f2, x0, x1!]);

      hence thesis;

    end;

    theorem :: DIFF_3:26

     [!((r (#) f1) + f2), x0, x1!] = ((r * [!f1, x0, x1!]) + [!f2, x0, x1!])

    proof

      set g = (r (#) f1);

       [!((r (#) f1) + f2), x0, x1!] = ( [!g, x0, x1!] + [!f2, x0, x1!]) by DIFF_1: 32

      .= ((r * [!f1, x0, x1!]) + [!f2, x0, x1!]) by DIFF_1: 31;

      hence thesis;

    end;

    theorem :: DIFF_3:27

     [!((r (#) f1) - f2), x0, x1!] = ((r * [!f1, x0, x1!]) - [!f2, x0, x1!])

    proof

      set g = (r (#) f1);

       [!((r (#) f1) - f2), x0, x1!] = ( [!g, x0, x1!] - [!f2, x0, x1!]) by Th25

      .= ((r * [!f1, x0, x1!]) - [!f2, x0, x1!]) by DIFF_1: 31;

      hence thesis;

    end;

    theorem :: DIFF_3:28

     [!(f1 + (r (#) f2)), x0, x1!] = ( [!f1, x0, x1!] + (r * [!f2, x0, x1!]))

    proof

      set g = (r (#) f2);

       [!(f1 + (r (#) f2)), x0, x1!] = ( [!f1, x0, x1!] + [!g, x0, x1!]) by DIFF_1: 32

      .= ( [!f1, x0, x1!] + (r * [!f2, x0, x1!])) by DIFF_1: 31;

      hence thesis;

    end;

    theorem :: DIFF_3:29

     [!(f1 - (r (#) f2)), x0, x1!] = ( [!f1, x0, x1!] - (r * [!f2, x0, x1!]))

    proof

      set g = (r (#) f2);

       [!(f1 - (r (#) f2)), x0, x1!] = ( [!f1, x0, x1!] - [!g, x0, x1!]) by Th25

      .= ( [!f1, x0, x1!] - (r * [!f2, x0, x1!])) by DIFF_1: 31;

      hence thesis;

    end;

    theorem :: DIFF_3:30

     [!((r1 (#) f1) - (r2 (#) f2)), x0, x1!] = ((r1 * [!f1, x0, x1!]) - (r2 * [!f2, x0, x1!]))

    proof

      set g1 = (r1 (#) f1);

      set g2 = (r2 (#) f2);

       [!((r1 (#) f1) - (r2 (#) f2)), x0, x1!] = ( [!g1, x0, x1!] - [!g2, x0, x1!]) by Th25

      .= ((r1 * [!f1, x0, x1!]) - [!g2, x0, x1!]) by DIFF_1: 31

      .= ((r1 * [!f1, x0, x1!]) - (r2 * [!f2, x0, x1!])) by DIFF_1: 31;

      hence thesis;

    end;

    theorem :: DIFF_3:31

    

     Th31: ((( bdif ((f1 (#) f2),h)) . 1) . x) = (((f1 . x) * ((( bdif (f2,h)) . 1) . x)) + ((f2 . (x - h)) * ((( bdif (f1,h)) . 1) . x)))

    proof

      ((( bdif ((f1 (#) f2),h)) . 1) . x) = ((( bdif ((f1 (#) f2),h)) . ( 0 + 1)) . x)

      .= (( bD ((( bdif ((f1 (#) f2),h)) . 0 ),h)) . x) by DIFF_1:def 7

      .= (( bD ((f1 (#) f2),h)) . x) by DIFF_1:def 7

      .= (((f1 (#) f2) . x) - ((f1 (#) f2) . (x - h))) by DIFF_1: 4

      .= (((f1 . x) * (f2 . x)) - ((f1 (#) f2) . (x - h))) by VALUED_1: 5

      .= (((f1 . x) * (f2 . x)) - ((f1 . (x - h)) * (f2 . (x - h)))) by VALUED_1: 5

      .= (((f1 . x) * ((f2 . x) - (f2 . (x - h)))) + ((f2 . (x - h)) * ((f1 . x) - (f1 . (x - h)))))

      .= (((f1 . x) * (( bD (f2,h)) . x)) + ((f2 . (x - h)) * ((f1 . x) - (f1 . (x - h))))) by DIFF_1: 4

      .= (((f1 . x) * (( bD (f2,h)) . x)) + ((f2 . (x - h)) * (( bD (f1,h)) . x))) by DIFF_1: 4

      .= (((f1 . x) * (( bD ((( bdif (f2,h)) . 0 ),h)) . x)) + ((f2 . (x - h)) * (( bD (f1,h)) . x))) by DIFF_1:def 7

      .= (((f1 . x) * (( bD ((( bdif (f2,h)) . 0 ),h)) . x)) + ((f2 . (x - h)) * (( bD ((( bdif (f1,h)) . 0 ),h)) . x))) by DIFF_1:def 7

      .= (((f1 . x) * ((( bdif (f2,h)) . ( 0 + 1)) . x)) + ((f2 . (x - h)) * (( bD ((( bdif (f1,h)) . 0 ),h)) . x))) by DIFF_1:def 7

      .= (((f1 . x) * ((( bdif (f2,h)) . 1) . x)) + ((f2 . (x - h)) * ((( bdif (f1,h)) . 1) . x))) by DIFF_1:def 7;

      hence thesis;

    end;

    theorem :: DIFF_3:32

    (x0,x1,x2) are_mutually_distinct implies [!f, x0, x1, x2!] = [!f, x0, x2, x1!]

    proof

      assume (x0,x1,x2) are_mutually_distinct ;

      then

       A1: (x2 - x1) <> 0 & (x2 - x0) <> 0 & (x1 - x0) <> 0 by ZFMISC_1:def 5;

      set x10 = (x1 - x0);

      set x20 = (x2 - x0);

      set x21 = (x2 - x1);

      

       A2: [!f, x0, x2, x1!] = (((((f . x0) - (f . x2)) / ( - (x2 - x0))) - (((f . x2) - (f . x1)) / (x2 - x1))) / ( - (x1 - x0)))

      .= ((( - (((f . x0) - (f . x2)) / (x2 - x0))) - (((f . x2) - (f . x1)) / (x2 - x1))) / ( - (x1 - x0))) by XCMPLX_1: 188

      .= (( - ((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x1)) / (x2 - x1)))) / ( - (x1 - x0)))

      .= (((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x1)) / (x2 - x1))) / (x1 - x0)) by XCMPLX_1: 191

      .= ((((((f . x0) - (f . x2)) * x21) + (((f . x2) - (f . x1)) * x20)) / (x20 * x21)) / x10) by A1, XCMPLX_1: 116

      .= (((((f . x0) * x21) - ((f . x1) * x20)) + ((f . x2) * x10)) / ((x20 * x21) * x10)) by XCMPLX_1: 78;

       [!f, x0, x1, x2!] = (((((f . x0) - (f . x1)) / ( - (x1 - x0))) - (((f . x1) - (f . x2)) / ( - (x2 - x1)))) / ( - (x2 - x0)))

      .= ((( - (((f . x0) - (f . x1)) / (x1 - x0))) - (((f . x1) - (f . x2)) / ( - (x2 - x1)))) / ( - (x2 - x0))) by XCMPLX_1: 188

      .= ((( - (((f . x0) - (f . x1)) / (x1 - x0))) - ( - (((f . x1) - (f . x2)) / (x2 - x1)))) / ( - (x2 - x0))) by XCMPLX_1: 188

      .= (( - ((((f . x0) - (f . x1)) / (x1 - x0)) - (((f . x1) - (f . x2)) / (x2 - x1)))) / ( - (x2 - x0)))

      .= (((((f . x0) - (f . x1)) / (x1 - x0)) - (((f . x1) - (f . x2)) / (x2 - x1))) / (x2 - x0)) by XCMPLX_1: 191

      .= ((((((f . x0) - (f . x1)) * x21) - (((f . x1) - (f . x2)) * x10)) / (x10 * x21)) / x20) by A1, XCMPLX_1: 130

      .= (((((f . x0) * x21) - ((f . x1) * x20)) + ((f . x2) * x10)) / ((x10 * x21) * x20)) by XCMPLX_1: 78

      .= [!f, x0, x2, x1!] by A2;

      hence thesis;

    end;

    reserve S for Seq_Sequence;

    theorem :: DIFF_3:33

    (for n,i be Nat st i <= n holds ((S . n) . i) = (((n choose i) * ((( bdif (f1,h)) . i) . x)) * ((( bdif (f2,h)) . (n -' i)) . (x - (i * h))))) implies ((( bdif ((f1 (#) f2),h)) . 1) . x) = ( Sum ((S . 1),1)) & ((( bdif ((f1 (#) f2),h)) . 2) . x) = ( Sum ((S . 2),2))

    proof

      assume

       A1: for n,i be Nat st i <= n holds ((S . n) . i) = (((n choose i) * ((( bdif (f1,h)) . i) . x)) * ((( bdif (f2,h)) . (n -' i)) . (x - (i * h))));

      

       A2: (1 -' 0 ) = (1 - 0 ) by XREAL_1: 233

      .= 1;

      

       A3: ((S . 1) . 0 ) = (((1 choose 0 ) * ((( bdif (f1,h)) . 0 ) . x)) * ((( bdif (f2,h)) . (1 -' 0 )) . (x - ( 0 * h)))) by A1

      .= ((1 * ((( bdif (f1,h)) . 0 ) . x)) * ((( bdif (f2,h)) . (1 -' 0 )) . (x - ( 0 * h)))) by NEWTON: 19

      .= ((f1 . x) * ((( bdif (f2,h)) . 1) . x)) by A2, DIFF_1:def 7;

      

       A4: (1 -' 1) = (1 - 1) by XREAL_1: 233

      .= 0 ;

      

       A5: ((S . 1) . 1) = (((1 choose 1) * ((( bdif (f1,h)) . 1) . x)) * ((( bdif (f2,h)) . (1 -' 1)) . (x - (1 * h)))) by A1

      .= ((1 * ((( bdif (f1,h)) . 1) . x)) * ((( bdif (f2,h)) . (1 -' 1)) . (x - (1 * h)))) by NEWTON: 21

      .= ((f2 . (x - h)) * ((( bdif (f1,h)) . 1) . x)) by A4, DIFF_1:def 7;

      

       A6: ( Sum ((S . 1),1)) = (( Partial_Sums (S . 1)) . ( 0 + 1)) by SERIES_1:def 5

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

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

      .= ((( bdif ((f1 (#) f2),h)) . 1) . x) by A3, A5, Th31;

      

       A7: (( bdif ((f1 (#) f2),h)) . 1) is Function of REAL , REAL by DIFF_1: 12;

      

       A8: (( bdif (f2,h)) . 1) is Function of REAL , REAL by DIFF_1: 12;

      

       A9: (( bdif (f1,h)) . 1) is Function of REAL , REAL by DIFF_1: 12;

      

       A10: ((( bdif ((f1 (#) f2),h)) . 2) . x) = ((( bdif ((f1 (#) f2),h)) . (1 + 1)) . x)

      .= (( bD ((( bdif ((f1 (#) f2),h)) . 1),h)) . x) by DIFF_1:def 7

      .= (((( bdif ((f1 (#) f2),h)) . 1) . x) - ((( bdif ((f1 (#) f2),h)) . 1) . (x - h))) by A7, DIFF_1: 4

      .= ((((f1 . x) * ((( bdif (f2,h)) . 1) . x)) + (((( bdif (f1,h)) . 1) . x) * (f2 . (x - h)))) - ((( bdif ((f1 (#) f2),h)) . 1) . (x - h))) by Th31

      .= ((((f1 . x) * ((( bdif (f2,h)) . 1) . x)) + (((( bdif (f1,h)) . 1) . x) * (f2 . (x - h)))) - (((f1 . (x - h)) * ((( bdif (f2,h)) . 1) . (x - h))) + (((( bdif (f1,h)) . 1) . (x - h)) * (f2 . ((x - h) - h))))) by Th31

      .= (((((f1 . x) * (((( bdif (f2,h)) . 1) . x) - ((( bdif (f2,h)) . 1) . (x - h)))) + (((f1 . x) - (f1 . (x - h))) * ((( bdif (f2,h)) . 1) . (x - h)))) - ((((( bdif (f1,h)) . 1) . (x - h)) - ((( bdif (f1,h)) . 1) . x)) * (f2 . (x - (2 * h))))) - (((( bdif (f1,h)) . 1) . x) * ((f2 . (x - (2 * h))) - (f2 . (x - h)))))

      .= (((((f1 . x) * (( bD ((( bdif (f2,h)) . 1),h)) . x)) + (((f1 . x) - (f1 . (x - h))) * ((( bdif (f2,h)) . 1) . (x - h)))) - ((((( bdif (f1,h)) . 1) . (x - h)) - ((( bdif (f1,h)) . 1) . x)) * (f2 . (x - (2 * h))))) - (((( bdif (f1,h)) . 1) . x) * ((f2 . (x - (2 * h))) - (f2 . (x - h))))) by A8, DIFF_1: 4

      .= (((((f1 . x) * (( bD ((( bdif (f2,h)) . 1),h)) . x)) + ((( bD (f1,h)) . x) * ((( bdif (f2,h)) . 1) . (x - h)))) + ((((( bdif (f1,h)) . 1) . x) - ((( bdif (f1,h)) . 1) . (x - h))) * (f2 . (x - (2 * h))))) - (((( bdif (f1,h)) . 1) . x) * ((f2 . (x - (2 * h))) - (f2 . (x - h))))) by DIFF_1: 4

      .= (((((f1 . x) * (( bD ((( bdif (f2,h)) . 1),h)) . x)) + ((( bD (f1,h)) . x) * ((( bdif (f2,h)) . 1) . (x - h)))) + ((( bD ((( bdif (f1,h)) . 1),h)) . x) * (f2 . (x - (2 * h))))) + (((( bdif (f1,h)) . 1) . x) * ((f2 . (x - h)) - (f2 . ((x - h) - h))))) by A9, DIFF_1: 4

      .= (((((f1 . x) * (( bD ((( bdif (f2,h)) . 1),h)) . x)) + ((( bD (f1,h)) . x) * ((( bdif (f2,h)) . 1) . (x - h)))) + ((( bD ((( bdif (f1,h)) . 1),h)) . x) * (f2 . (x - (2 * h))))) + (((( bdif (f1,h)) . 1) . x) * (( bD (f2,h)) . (x - h)))) by DIFF_1: 4

      .= (((((f1 . x) * ((( bdif (f2,h)) . (1 + 1)) . x)) + ((( bD (f1,h)) . x) * ((( bdif (f2,h)) . 1) . (x - h)))) + ((( bD ((( bdif (f1,h)) . 1),h)) . x) * (f2 . (x - (2 * h))))) + (((( bdif (f1,h)) . 1) . x) * (( bD (f2,h)) . (x - h)))) by DIFF_1:def 7

      .= (((((f1 . x) * ((( bdif (f2,h)) . (1 + 1)) . x)) + ((( bD ((( bdif (f1,h)) . 0 ),h)) . x) * ((( bdif (f2,h)) . 1) . (x - h)))) + ((( bD ((( bdif (f1,h)) . 1),h)) . x) * (f2 . (x - (2 * h))))) + (((( bdif (f1,h)) . 1) . x) * (( bD (f2,h)) . (x - h)))) by DIFF_1:def 7

      .= (((((f1 . x) * ((( bdif (f2,h)) . 2) . x)) + ((( bD ((( bdif (f1,h)) . 0 ),h)) . x) * ((( bdif (f2,h)) . 1) . (x - h)))) + (((( bdif (f1,h)) . 2) . x) * (f2 . (x - (2 * h))))) + (((( bdif (f1,h)) . 1) . x) * (( bD (f2,h)) . (x - h)))) by DIFF_1:def 7

      .= (((((f1 . x) * ((( bdif (f2,h)) . 2) . x)) + (((( bdif (f1,h)) . ( 0 + 1)) . x) * ((( bdif (f2,h)) . 1) . (x - h)))) + (((( bdif (f1,h)) . 2) . x) * (f2 . (x - (2 * h))))) + (((( bdif (f1,h)) . 1) . x) * (( bD (f2,h)) . (x - h)))) by DIFF_1:def 7

      .= (((((f1 . x) * ((( bdif (f2,h)) . 2) . x)) + (((( bdif (f1,h)) . 1) . x) * ((( bdif (f2,h)) . 1) . (x - h)))) + (((( bdif (f1,h)) . 2) . x) * (f2 . (x - (2 * h))))) + (((( bdif (f1,h)) . 1) . x) * (( bD ((( bdif (f2,h)) . 0 ),h)) . (x - h)))) by DIFF_1:def 7

      .= (((((f1 . x) * ((( bdif (f2,h)) . 2) . x)) + (((( bdif (f1,h)) . 1) . x) * ((( bdif (f2,h)) . 1) . (x - h)))) + (((( bdif (f1,h)) . 2) . x) * (f2 . (x - (2 * h))))) + (((( bdif (f1,h)) . 1) . x) * ((( bdif (f2,h)) . ( 0 + 1)) . (x - h)))) by DIFF_1:def 7

      .= ((((f1 . x) * ((( bdif (f2,h)) . 2) . x)) + (2 * (((( bdif (f1,h)) . 1) . x) * ((( bdif (f2,h)) . 1) . (x - h))))) + (((( bdif (f1,h)) . 2) . x) * (f2 . (x - (2 * h)))));

      

       A11: (2 -' 0 ) = (2 - 0 ) by XREAL_1: 233

      .= 2;

      

       A12: ((S . 2) . 0 ) = (((2 choose 0 ) * ((( bdif (f1,h)) . 0 ) . x)) * ((( bdif (f2,h)) . (2 -' 0 )) . (x - ( 0 * h)))) by A1

      .= ((1 * ((( bdif (f1,h)) . 0 ) . x)) * ((( bdif (f2,h)) . (2 -' 0 )) . (x - ( 0 * h)))) by NEWTON: 19

      .= ((f1 . x) * ((( bdif (f2,h)) . 2) . x)) by A11, DIFF_1:def 7;

      

       A13: (2 -' 1) = (2 - 1) by XREAL_1: 233

      .= 1;

      

       A14: ((S . 2) . 1) = (((2 choose 1) * ((( bdif (f1,h)) . 1) . x)) * ((( bdif (f2,h)) . (2 -' 1)) . (x - (1 * h)))) by A1

      .= ((2 * ((( bdif (f1,h)) . 1) . x)) * ((( bdif (f2,h)) . 1) . (x - h))) by A13, NEWTON: 23;

      

       A15: (2 -' 2) = (2 - 2) by XREAL_1: 233

      .= 0 ;

      

       A16: ((S . 2) . 2) = (((2 choose 2) * ((( bdif (f1,h)) . 2) . x)) * ((( bdif (f2,h)) . (2 -' 2)) . (x - (2 * h)))) by A1

      .= ((1 * ((( bdif (f1,h)) . 2) . x)) * ((( bdif (f2,h)) . (2 -' 2)) . (x - (2 * h)))) by NEWTON: 21

      .= (((( bdif (f1,h)) . 2) . x) * (f2 . (x - (2 * h)))) by A15, DIFF_1:def 7;

      ( Sum ((S . 2),2)) = (( Partial_Sums (S . 2)) . (1 + 1)) by SERIES_1:def 5

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

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

      .= ((( bdif ((f1 (#) f2),h)) . 2) . x) by A10, A12, A14, A16, SERIES_1:def 1;

      hence thesis by A6;

    end;

    theorem :: DIFF_3:34

    

     Th34: ((( cdif ((f1 (#) f2),h)) . 1) . x) = (((f1 . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . x)) + ((f2 . (x - (h / 2))) * ((( cdif (f1,h)) . 1) . x)))

    proof

      ((( cdif ((f1 (#) f2),h)) . 1) . x) = ((( cdif ((f1 (#) f2),h)) . ( 0 + 1)) . x)

      .= (( cD ((( cdif ((f1 (#) f2),h)) . 0 ),h)) . x) by DIFF_1:def 8

      .= (( cD ((f1 (#) f2),h)) . x) by DIFF_1:def 8

      .= (((f1 (#) f2) . (x + (h / 2))) - ((f1 (#) f2) . (x - (h / 2)))) by DIFF_1: 5

      .= (((f1 . (x + (h / 2))) * (f2 . (x + (h / 2)))) - ((f1 (#) f2) . (x - (h / 2)))) by VALUED_1: 5

      .= (((f1 . (x + (h / 2))) * (f2 . (x + (h / 2)))) - ((f1 . (x - (h / 2))) * (f2 . (x - (h / 2))))) by VALUED_1: 5

      .= (((f1 . (x + (h / 2))) * ((f2 . (x + (h / 2))) - (f2 . (x - (h / 2))))) + ((f2 . (x - (h / 2))) * ((f1 . (x + (h / 2))) - (f1 . (x - (h / 2))))))

      .= (((f1 . (x + (h / 2))) * (( cD (f2,h)) . x)) + ((f2 . (x - (h / 2))) * ((f1 . (x + (h / 2))) - (f1 . (x - (h / 2)))))) by DIFF_1: 5

      .= (((f1 . (x + (h / 2))) * (( cD (f2,h)) . x)) + ((f2 . (x - (h / 2))) * (( cD (f1,h)) . x))) by DIFF_1: 5

      .= (((f1 . (x + (h / 2))) * (( cD ((( cdif (f2,h)) . 0 ),h)) . x)) + ((f2 . (x - (h / 2))) * (( cD (f1,h)) . x))) by DIFF_1:def 8

      .= (((f1 . (x + (h / 2))) * (( cD ((( cdif (f2,h)) . 0 ),h)) . x)) + ((f2 . (x - (h / 2))) * (( cD ((( cdif (f1,h)) . 0 ),h)) . x))) by DIFF_1:def 8

      .= (((f1 . (x + (h / 2))) * ((( cdif (f2,h)) . ( 0 + 1)) . x)) + ((f2 . (x - (h / 2))) * (( cD ((( cdif (f1,h)) . 0 ),h)) . x))) by DIFF_1:def 8

      .= (((f1 . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . x)) + ((f2 . (x - (h / 2))) * ((( cdif (f1,h)) . 1) . x))) by DIFF_1:def 8;

      hence thesis;

    end;

    theorem :: DIFF_3:35

    (for n,i be Nat st i <= n holds ((S . n) . i) = (((n choose i) * ((( cdif (f1,h)) . i) . (x + ((n -' i) * (h / 2))))) * ((( cdif (f2,h)) . (n -' i)) . (x - (i * (h / 2)))))) implies ((( cdif ((f1 (#) f2),h)) . 1) . x) = ( Sum ((S . 1),1)) & ((( cdif ((f1 (#) f2),h)) . 2) . x) = ( Sum ((S . 2),2))

    proof

      assume

       A1: for n,i be Nat st i <= n holds ((S . n) . i) = (((n choose i) * ((( cdif (f1,h)) . i) . (x + ((n -' i) * (h / 2))))) * ((( cdif (f2,h)) . (n -' i)) . (x - (i * (h / 2)))));

      

       A2: (1 -' 0 ) = (1 - 0 ) by XREAL_1: 233

      .= 1;

      

       A3: ((S . 1) . 0 ) = (((1 choose 0 ) * ((( cdif (f1,h)) . 0 ) . (x + ((1 -' 0 ) * (h / 2))))) * ((( cdif (f2,h)) . (1 -' 0 )) . (x - ( 0 * (h / 2))))) by A1

      .= ((1 * ((( cdif (f1,h)) . 0 ) . (x + ((1 -' 0 ) * (h / 2))))) * ((( cdif (f2,h)) . (1 -' 0 )) . (x - ( 0 * (h / 2))))) by NEWTON: 19

      .= ((f1 . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . x)) by A2, DIFF_1:def 8;

      

       A4: (1 -' 1) = (1 - 1) by XREAL_1: 233

      .= 0 ;

      

       A5: ((S . 1) . 1) = (((1 choose 1) * ((( cdif (f1,h)) . 1) . (x + ((1 -' 1) * (h / 2))))) * ((( cdif (f2,h)) . (1 -' 1)) . (x - (1 * (h / 2))))) by A1

      .= ((1 * ((( cdif (f1,h)) . 1) . (x + ((1 -' 1) * (h / 2))))) * ((( cdif (f2,h)) . (1 -' 1)) . (x - (1 * (h / 2))))) by NEWTON: 21

      .= ((f2 . (x - (h / 2))) * ((( cdif (f1,h)) . 1) . x)) by A4, DIFF_1:def 8;

      

       A6: ( Sum ((S . 1),1)) = (( Partial_Sums (S . 1)) . ( 0 + 1)) by SERIES_1:def 5

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

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

      .= ((( cdif ((f1 (#) f2),h)) . 1) . x) by A3, A5, Th34;

      

       A7: (( cdif ((f1 (#) f2),h)) . 1) is Function of REAL , REAL by DIFF_1: 19;

      

       A8: (( cdif (f1,h)) . 1) is Function of REAL , REAL by DIFF_1: 19;

      

       A9: (( cdif (f2,h)) . 1) is Function of REAL , REAL by DIFF_1: 19;

      

       A10: ((( cdif ((f1 (#) f2),h)) . 2) . x) = ((( cdif ((f1 (#) f2),h)) . (1 + 1)) . x)

      .= (( cD ((( cdif ((f1 (#) f2),h)) . 1),h)) . x) by DIFF_1:def 8

      .= (((( cdif ((f1 (#) f2),h)) . 1) . (x + (h / 2))) - ((( cdif ((f1 (#) f2),h)) . 1) . (x - (h / 2)))) by A7, DIFF_1: 5

      .= ((((f1 . ((x + (h / 2)) + (h / 2))) * ((( cdif (f2,h)) . 1) . (x + (h / 2)))) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * (f2 . ((x + (h / 2)) - (h / 2))))) - ((( cdif ((f1 (#) f2),h)) . 1) . (x - (h / 2)))) by Th34

      .= ((((f1 . (x + h)) * ((( cdif (f2,h)) . 1) . (x + (h / 2)))) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * (f2 . x))) - (((f1 . ((x - (h / 2)) + (h / 2))) * ((( cdif (f2,h)) . 1) . (x - (h / 2)))) + (((( cdif (f1,h)) . 1) . (x - (h / 2))) * (f2 . ((x - (h / 2)) - (h / 2)))))) by Th34

      .= (((((f1 . (x + h)) * (((( cdif (f2,h)) . 1) . (x + (h / 2))) - ((( cdif (f2,h)) . 1) . (x - (h / 2))))) + (((f1 . (x + h)) - (f1 . x)) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) - ((((( cdif (f1,h)) . 1) . (x - (h / 2))) - ((( cdif (f1,h)) . 1) . (x + (h / 2)))) * (f2 . (x - h)))) - (((( cdif (f1,h)) . 1) . (x + (h / 2))) * ((f2 . (x - h)) - (f2 . x))))

      .= (((((f1 . (x + h)) * (( cD ((( cdif (f2,h)) . 1),h)) . x)) + (((f1 . ((x + (h / 2)) + (h / 2))) - (f1 . ((x + (h / 2)) - (h / 2)))) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) - ((((( cdif (f1,h)) . 1) . (x - (h / 2))) - ((( cdif (f1,h)) . 1) . (x + (h / 2)))) * (f2 . (x - h)))) - (((( cdif (f1,h)) . 1) . (x + (h / 2))) * ((f2 . (x - h)) - (f2 . x)))) by A9, DIFF_1: 5

      .= (((((f1 . (x + h)) * (( cD ((( cdif (f2,h)) . 1),h)) . x)) + ((( cD (f1,h)) . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) + ((((( cdif (f1,h)) . 1) . (x + (h / 2))) - ((( cdif (f1,h)) . 1) . (x - (h / 2)))) * (f2 . (x - h)))) - (((( cdif (f1,h)) . 1) . (x + (h / 2))) * ((f2 . (x - h)) - (f2 . x)))) by DIFF_1: 5

      .= (((((f1 . (x + h)) * (( cD ((( cdif (f2,h)) . 1),h)) . x)) + ((( cD (f1,h)) . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) + ((( cD ((( cdif (f1,h)) . 1),h)) . x) * (f2 . (x - h)))) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * ((f2 . ((x - (h / 2)) + (h / 2))) - (f2 . ((x - (h / 2)) - (h / 2)))))) by A8, DIFF_1: 5

      .= (((((f1 . (x + h)) * (( cD ((( cdif (f2,h)) . 1),h)) . x)) + ((( cD (f1,h)) . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) + ((( cD ((( cdif (f1,h)) . 1),h)) . x) * (f2 . (x - h)))) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * (( cD (f2,h)) . (x - (h / 2))))) by DIFF_1: 5

      .= (((((f1 . (x + h)) * ((( cdif (f2,h)) . (1 + 1)) . x)) + ((( cD (f1,h)) . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) + ((( cD ((( cdif (f1,h)) . 1),h)) . x) * (f2 . (x - h)))) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * (( cD (f2,h)) . (x - (h / 2))))) by DIFF_1:def 8

      .= (((((f1 . (x + h)) * ((( cdif (f2,h)) . 2) . x)) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) + ((( cD ((( cdif (f1,h)) . 1),h)) . x) * (f2 . (x - h)))) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * (( cD (f2,h)) . (x - (h / 2))))) by Th16

      .= (((((f1 . (x + h)) * ((( cdif (f2,h)) . 2) . x)) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) + (((( cdif (f1,h)) . (1 + 1)) . x) * (f2 . (x - h)))) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * (( cD (f2,h)) . (x - (h / 2))))) by DIFF_1:def 8

      .= (((((f1 . (x + h)) * ((( cdif (f2,h)) . 2) . x)) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) + (((( cdif (f1,h)) . 2) . x) * (f2 . (x - h)))) + (((( cdif (f1,h)) . 1) . (x + (h / 2))) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) by Th16

      .= ((((f1 . (x + h)) * ((( cdif (f2,h)) . 2) . x)) + ((2 * ((( cdif (f1,h)) . 1) . (x + (h / 2)))) * ((( cdif (f2,h)) . 1) . (x - (h / 2))))) + (((( cdif (f1,h)) . 2) . x) * (f2 . (x - h))));

      

       A11: (2 -' 0 ) = (2 - 0 ) by XREAL_1: 233

      .= 2;

      

       A12: ((S . 2) . 0 ) = (((2 choose 0 ) * ((( cdif (f1,h)) . 0 ) . (x + ((2 -' 0 ) * (h / 2))))) * ((( cdif (f2,h)) . (2 -' 0 )) . (x - ( 0 * (h / 2))))) by A1

      .= ((1 * ((( cdif (f1,h)) . 0 ) . (x + ((2 -' 0 ) * (h / 2))))) * ((( cdif (f2,h)) . (2 -' 0 )) . (x - ( 0 * (h / 2))))) by NEWTON: 19

      .= ((f1 . (x + h)) * ((( cdif (f2,h)) . 2) . x)) by A11, DIFF_1:def 8;

      

       A13: (2 -' 1) = (2 - 1) by XREAL_1: 233

      .= 1;

      

       A14: ((S . 2) . 1) = (((2 choose 1) * ((( cdif (f1,h)) . 1) . (x + ((2 -' 1) * (h / 2))))) * ((( cdif (f2,h)) . (2 -' 1)) . (x - (1 * (h / 2))))) by A1

      .= ((2 * ((( cdif (f1,h)) . 1) . (x + (h / 2)))) * ((( cdif (f2,h)) . 1) . (x - (h / 2)))) by A13, NEWTON: 23;

      

       A15: (2 -' 2) = (2 - 2) by XREAL_1: 233

      .= 0 ;

      

       A16: ((S . 2) . 2) = (((2 choose 2) * ((( cdif (f1,h)) . 2) . (x + ((2 -' 2) * (h / 2))))) * ((( cdif (f2,h)) . (2 -' 2)) . (x - (2 * (h / 2))))) by A1

      .= ((1 * ((( cdif (f1,h)) . 2) . (x + ((2 -' 2) * (h / 2))))) * ((( cdif (f2,h)) . (2 -' 2)) . (x - (2 * (h / 2))))) by NEWTON: 21

      .= (((( cdif (f1,h)) . 2) . x) * (f2 . (x - h))) by A15, DIFF_1:def 8;

      ( Sum ((S . 2),2)) = (( Partial_Sums (S . 2)) . (1 + 1)) by SERIES_1:def 5

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

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

      .= ((( cdif ((f1 (#) f2),h)) . 2) . x) by A10, A12, A14, A16, SERIES_1:def 1;

      hence thesis by A6;

    end;

    theorem :: DIFF_3:36

    (for x holds (f . x) = ( sqrt x)) & x0 <> x1 & x0 > 0 & x1 > 0 implies [!f, x0, x1!] = (1 / (( sqrt x0) + ( sqrt x1)))

    proof

      assume that

       A1: for x holds (f . x) = ( sqrt x) and

       A2: x0 <> x1 and

       A3: x0 > 0 & x1 > 0 ;

       [!f, x0, x1!] = ((( sqrt x0) - (f . x1)) / (x0 - x1)) by A1

      .= ((( sqrt x0) - ( sqrt x1)) / (x0 - x1)) by A1

      .= (1 / (( sqrt x0) + ( sqrt x1))) by A2, A3, SQUARE_1: 36;

      hence thesis;

    end;

    theorem :: DIFF_3:37

    (for x holds (f . x) = ( sqrt x)) & (x0,x1,x2) are_mutually_distinct & x0 > 0 & x1 > 0 & x2 > 0 implies [!f, x0, x1, x2!] = ( - (1 / (((( sqrt x0) + ( sqrt x1)) * (( sqrt x0) + ( sqrt x2))) * (( sqrt x1) + ( sqrt x2)))))

    proof

      assume that

       A1: for x holds (f . x) = ( sqrt x) and

       A2: (x0,x1,x2) are_mutually_distinct and

       A3: x0 > 0 & x1 > 0 & x2 > 0 ;

      

       A4: (f . x0) = ( sqrt x0) & (f . x1) = ( sqrt x1) & (f . x2) = ( sqrt x2) by A1;

      ( sqrt x0) > 0 & ( sqrt x1) > 0 & ( sqrt x2) > 0 by A3, SQUARE_1: 25;

      then

       A5: (( sqrt x0) + ( sqrt x1)) > 0 & (( sqrt x1) + ( sqrt x2)) > 0 ;

      

       A6: x0 <> x1 & x1 <> x2 & x2 <> x0 by A2, ZFMISC_1:def 5;

      

      then [!f, x0, x1, x2!] = (((1 / (( sqrt x0) + ( sqrt x1))) - ((( sqrt x1) - ( sqrt x2)) / (x1 - x2))) / (x0 - x2)) by A3, A4, SQUARE_1: 36

      .= (((1 / (( sqrt x0) + ( sqrt x1))) - (1 / (( sqrt x1) + ( sqrt x2)))) / (x0 - x2)) by A3, A6, SQUARE_1: 36

      .= ((((1 * (( sqrt x1) + ( sqrt x2))) - (1 * (( sqrt x0) + ( sqrt x1)))) / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) / (x0 - x2)) by A5, XCMPLX_1: 130

      .= (((( sqrt x2) - ( sqrt x0)) / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) / ( - (x2 - x0)))

      .= ( - (((( sqrt x2) - ( sqrt x0)) / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) / (x2 - x0))) by XCMPLX_1: 188

      .= ( - ((1 / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) * ((( sqrt x2) - ( sqrt x0)) / (x2 - x0))))

      .= ( - ((1 / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) * (1 / (( sqrt x2) + ( sqrt x0))))) by A3, A6, SQUARE_1: 36

      .= ( - (1 / (((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))))) by XCMPLX_1: 102;

      hence thesis;

    end;

    theorem :: DIFF_3:38

    (for x holds (f . x) = ( sqrt x)) & (x0,x1,x2,x3) are_mutually_distinct & x0 > 0 & x1 > 0 & x2 > 0 & x3 > 0 implies [!f, x0, x1, x2, x3!] = ((((( sqrt x0) + ( sqrt x1)) + ( sqrt x2)) + ( sqrt x3)) / ((((((( sqrt x0) + ( sqrt x1)) * (( sqrt x0) + ( sqrt x2))) * (( sqrt x0) + ( sqrt x3))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x1) + ( sqrt x3))) * (( sqrt x2) + ( sqrt x3))))

    proof

      assume that

       A1: for x holds (f . x) = ( sqrt x) and

       A2: (x0,x1,x2,x3) are_mutually_distinct and

       A3: x0 > 0 & x1 > 0 & x2 > 0 & x3 > 0 ;

      

       A4: (f . x0) = ( sqrt x0) & (f . x1) = ( sqrt x1) & (f . x2) = ( sqrt x2) & (f . x3) = ( sqrt x3) by A1;

      ( sqrt x0) > 0 & ( sqrt x1) > 0 & ( sqrt x2) > 0 & ( sqrt x3) > 0 by A3, SQUARE_1: 25;

      then

       A5: (( sqrt x0) + ( sqrt x1)) > 0 & (( sqrt x1) + ( sqrt x2)) > 0 & (( sqrt x2) + ( sqrt x3)) > 0 & (( sqrt x2) + ( sqrt x0)) > 0 & (( sqrt x3) + ( sqrt x1)) > 0 ;

      

       A6: x0 <> x1 & x0 <> x2 & x0 <> x3 & x1 <> x2 & x1 <> x3 & x2 <> x3 by A2, ZFMISC_1:def 6;

      

      then [!f, x0, x1, x2, x3!] = (((((1 / (( sqrt x0) + ( sqrt x1))) - ((( sqrt x1) - ( sqrt x2)) / (x1 - x2))) / (x0 - x2)) - ((((( sqrt x1) - ( sqrt x2)) / (x1 - x2)) - ((( sqrt x2) - ( sqrt x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)) by A3, A4, SQUARE_1: 36

      .= (((((1 / (( sqrt x0) + ( sqrt x1))) - (1 / (( sqrt x1) + ( sqrt x2)))) / (x0 - x2)) - ((((( sqrt x1) - ( sqrt x2)) / (x1 - x2)) - ((( sqrt x2) - ( sqrt x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)) by A3, A6, SQUARE_1: 36

      .= (((((1 / (( sqrt x0) + ( sqrt x1))) - (1 / (( sqrt x1) + ( sqrt x2)))) / (x0 - x2)) - (((1 / (( sqrt x1) + ( sqrt x2))) - ((( sqrt x2) - ( sqrt x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)) by A3, A6, SQUARE_1: 36

      .= (((((1 / (( sqrt x0) + ( sqrt x1))) - (1 / (( sqrt x1) + ( sqrt x2)))) / (x0 - x2)) - (((1 / (( sqrt x1) + ( sqrt x2))) - (1 / (( sqrt x2) + ( sqrt x3)))) / (x1 - x3))) / (x0 - x3)) by A3, A6, SQUARE_1: 36

      .= ((((((1 * (( sqrt x1) + ( sqrt x2))) - (1 * (( sqrt x0) + ( sqrt x1)))) / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) / (x0 - x2)) - (((1 / (( sqrt x1) + ( sqrt x2))) - (1 / (( sqrt x2) + ( sqrt x3)))) / (x1 - x3))) / (x0 - x3)) by A5, XCMPLX_1: 130

      .= ((((((1 * (( sqrt x1) + ( sqrt x2))) - (1 * (( sqrt x0) + ( sqrt x1)))) / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) / (x0 - x2)) - ((((1 * (( sqrt x2) + ( sqrt x3))) - (1 * (( sqrt x1) + ( sqrt x2)))) / ((( sqrt x1) + ( sqrt x2)) * (( sqrt x2) + ( sqrt x3)))) / (x1 - x3))) / (x0 - x3)) by A5, XCMPLX_1: 130

      .= (((((( sqrt x2) - ( sqrt x0)) / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) / ( - (x2 - x0))) - (((( sqrt x3) - ( sqrt x1)) / ((( sqrt x1) + ( sqrt x2)) * (( sqrt x2) + ( sqrt x3)))) / ( - (x3 - x1)))) / (x0 - x3))

      .= ((( - (((( sqrt x2) - ( sqrt x0)) / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) / (x2 - x0))) - (((( sqrt x3) - ( sqrt x1)) / ((( sqrt x1) + ( sqrt x2)) * (( sqrt x2) + ( sqrt x3)))) / ( - (x3 - x1)))) / (x0 - x3)) by XCMPLX_1: 188

      .= ((( - ((1 / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) * ((( sqrt x2) - ( sqrt x0)) / (x2 - x0)))) - ( - (((( sqrt x3) - ( sqrt x1)) / ((( sqrt x1) + ( sqrt x2)) * (( sqrt x2) + ( sqrt x3)))) / (x3 - x1)))) / (x0 - x3)) by XCMPLX_1: 188

      .= ((( - ((1 / ((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2)))) * (1 / (( sqrt x2) + ( sqrt x0))))) - ( - (((( sqrt x3) - ( sqrt x1)) / ((( sqrt x1) + ( sqrt x2)) * (( sqrt x2) + ( sqrt x3)))) / (x3 - x1)))) / (x0 - x3)) by A3, A6, SQUARE_1: 36

      .= ((( - (1 / (((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))))) + ((1 / ((( sqrt x1) + ( sqrt x2)) * (( sqrt x2) + ( sqrt x3)))) * ((( sqrt x3) - ( sqrt x1)) / (x3 - x1)))) / (x0 - x3)) by XCMPLX_1: 102

      .= ((( - (1 / (((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))))) + ((1 / ((( sqrt x1) + ( sqrt x2)) * (( sqrt x2) + ( sqrt x3)))) * (1 / (( sqrt x3) + ( sqrt x1))))) / (x0 - x3)) by A3, A6, SQUARE_1: 36

      .= (((1 / (((( sqrt x1) + ( sqrt x2)) * (( sqrt x2) + ( sqrt x3))) * (( sqrt x3) + ( sqrt x1)))) - (1 / (((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))))) / (x0 - x3)) by XCMPLX_1: 102

      .= ((((1 * (((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0)))) - (1 * (((( sqrt x1) + ( sqrt x2)) * (( sqrt x2) + ( sqrt x3))) * (( sqrt x3) + ( sqrt x1))))) / ((((( sqrt x1) + ( sqrt x2)) * (( sqrt x2) + ( sqrt x3))) * (( sqrt x3) + ( sqrt x1))) * (((( sqrt x0) + ( sqrt x1)) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))))) / (x0 - x3)) by A5, XCMPLX_1: 130

      .= ((((((( sqrt x0) + ( sqrt x1)) * (( sqrt x2) + ( sqrt x0))) - ((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1)))) * (( sqrt x1) + ( sqrt x2))) / ((((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))) * (( sqrt x1) + ( sqrt x2)))) / (x0 - x3))

      .= (((((((( sqrt x0) * ( sqrt x2)) + (( sqrt x0) * ( sqrt x0))) + (( sqrt x1) * ( sqrt x2))) + (( sqrt x1) * ( sqrt x0))) - ((((( sqrt x2) * ( sqrt x3)) + (( sqrt x2) * ( sqrt x1))) + (( sqrt x3) * ( sqrt x3))) + (( sqrt x3) * ( sqrt x1)))) / (((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0)))) / (x0 - x3)) by A5, XCMPLX_1: 91

      .= (((((((( sqrt x0) * ( sqrt x2)) + ( sqrt (x0 ^2 ))) + (( sqrt x1) * ( sqrt x2))) + (( sqrt x1) * ( sqrt x0))) - ((((( sqrt x2) * ( sqrt x3)) + (( sqrt x2) * ( sqrt x1))) + (( sqrt x3) * ( sqrt x3))) + (( sqrt x3) * ( sqrt x1)))) / (((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0)))) / (x0 - x3)) by A3, SQUARE_1: 29

      .= (((((((( sqrt x0) * ( sqrt x2)) + x0) + (( sqrt x1) * ( sqrt x2))) + (( sqrt x1) * ( sqrt x0))) - ((((( sqrt x2) * ( sqrt x3)) + (( sqrt x2) * ( sqrt x1))) + (( sqrt x3) * ( sqrt x3))) + (( sqrt x3) * ( sqrt x1)))) / (((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0)))) / (x0 - x3)) by A3, SQUARE_1: 22

      .= (((((((( sqrt x0) * ( sqrt x2)) + x0) + (( sqrt x1) * ( sqrt x2))) + (( sqrt x1) * ( sqrt x0))) - ((((( sqrt x2) * ( sqrt x3)) + (( sqrt x2) * ( sqrt x1))) + ( sqrt (x3 ^2 ))) + (( sqrt x3) * ( sqrt x1)))) / (((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0)))) / (x0 - x3)) by A3, SQUARE_1: 29

      .= (((((((( sqrt x0) * ( sqrt x2)) + x0) + (( sqrt x1) * ( sqrt x2))) + (( sqrt x1) * ( sqrt x0))) - ((((( sqrt x2) * ( sqrt x3)) + (( sqrt x2) * ( sqrt x1))) + x3) + (( sqrt x3) * ( sqrt x1)))) / (((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0)))) / (x0 - x3)) by A3, SQUARE_1: 22

      .= ((((( sqrt x2) + ( sqrt x1)) * (( sqrt x0) - ( sqrt x3))) + (x0 - x3)) / ((((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))) * (x0 - x3))) by XCMPLX_1: 78

      .= ((((( sqrt x0) - ( sqrt x3)) * (( sqrt x2) + ( sqrt x1))) + ((( sqrt x0) - ( sqrt x3)) * (( sqrt x0) + ( sqrt x3)))) / ((((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))) * (x0 - x3))) by A3, SQUARE_1: 35

      .= (((( sqrt x0) - ( sqrt x3)) * (((( sqrt x2) + ( sqrt x1)) + ( sqrt x0)) + ( sqrt x3))) / ((((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))) * (x0 - x3)))

      .= (((( sqrt x0) - ( sqrt x3)) / (x0 - x3)) * ((((( sqrt x2) + ( sqrt x1)) + ( sqrt x0)) + ( sqrt x3)) / (((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))))) by XCMPLX_1: 76

      .= ((1 / (( sqrt x0) + ( sqrt x3))) * ((((( sqrt x2) + ( sqrt x1)) + ( sqrt x0)) + ( sqrt x3)) / (((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))))) by A3, A6, SQUARE_1: 36

      .= ((((( sqrt x2) + ( sqrt x1)) + ( sqrt x0)) + ( sqrt x3)) / ((((((( sqrt x2) + ( sqrt x3)) * (( sqrt x3) + ( sqrt x1))) * (( sqrt x0) + ( sqrt x1))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x2) + ( sqrt x0))) * (( sqrt x0) + ( sqrt x3)))) by XCMPLX_1: 103

      .= ((((( sqrt x0) + ( sqrt x1)) + ( sqrt x2)) + ( sqrt x3)) / ((((((( sqrt x0) + ( sqrt x1)) * (( sqrt x0) + ( sqrt x2))) * (( sqrt x0) + ( sqrt x3))) * (( sqrt x1) + ( sqrt x2))) * (( sqrt x1) + ( sqrt x3))) * (( sqrt x2) + ( sqrt x3))));

      hence thesis;

    end;

    theorem :: DIFF_3:39

    (for x holds (f . x) = ( sqrt x)) & x > 0 & (x + h) > 0 implies (( fD (f,h)) . x) = (( sqrt (x + h)) - ( sqrt x))

    proof

      assume

       A1: for x holds (f . x) = ( sqrt x);

      (( fD (f,h)) . x) = ((f . (x + h)) - (f . x)) by DIFF_1: 3

      .= (( sqrt (x + h)) - (f . x)) by A1

      .= (( sqrt (x + h)) - ( sqrt x)) by A1;

      hence thesis;

    end;

    theorem :: DIFF_3:40

    (for x holds (f . x) = ( sqrt x)) & x > 0 & (x - h) > 0 implies (( bD (f,h)) . x) = (( sqrt x) - ( sqrt (x - h)))

    proof

      assume

       A1: for x holds (f . x) = ( sqrt x);

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= (( sqrt x) - (f . (x - h))) by A1

      .= (( sqrt x) - ( sqrt (x - h))) by A1;

      hence thesis;

    end;

    theorem :: DIFF_3:41

    (for x holds (f . x) = ( sqrt x)) & (x + (h / 2)) > 0 & (x - (h / 2)) > 0 implies (( cD (f,h)) . x) = (( sqrt (x + (h / 2))) - ( sqrt (x - (h / 2))))

    proof

      assume

       A1: for x holds (f . x) = ( sqrt x);

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= (( sqrt (x + (h / 2))) - (f . (x - (h / 2)))) by A1

      .= (( sqrt (x + (h / 2))) - ( sqrt (x - (h / 2)))) by A1;

      hence thesis;

    end;

    theorem :: DIFF_3:42

    (for x holds (f . x) = (x ^2 )) & x0 <> x1 implies [!f, x0, x1!] = (x0 + x1)

    proof

      assume that

       A1: for x holds (f . x) = (x ^2 ) and

       A2: x0 <> x1;

      

       A3: (x0 - x1) <> 0 by A2;

       [!f, x0, x1!] = (((x0 ^2 ) - (f . x1)) / (x0 - x1)) by A1

      .= (((x0 ^2 ) - (x1 ^2 )) / (x0 - x1)) by A1

      .= (((x0 - x1) * (x0 + x1)) / (x0 - x1))

      .= (x0 + x1) by A3, XCMPLX_1: 89;

      hence thesis;

    end;

    theorem :: DIFF_3:43

    (for x holds (f . x) = (x ^2 )) & (x0,x1,x2) are_mutually_distinct implies [!f, x0, x1, x2!] = 1

    proof

      assume that

       A1: for x holds (f . x) = (x ^2 ) and

       A2: (x0,x1,x2) are_mutually_distinct ;

      

       A3: (f . x0) = (x0 ^2 ) & (f . x1) = (x1 ^2 ) & (f . x2) = (x2 ^2 ) by A1;

      

       A4: (x0 - x1) <> 0 & (x1 - x2) <> 0 & (x0 - x2) <> 0 by A2, ZFMISC_1:def 5;

       [!f, x0, x1, x2!] = (((((x0 - x1) * (x0 + x1)) / (x0 - x1)) - (((x1 - x2) * (x1 + x2)) / (x1 - x2))) / (x0 - x2)) by A3

      .= (((x0 + x1) - (((x1 - x2) * (x1 + x2)) / (x1 - x2))) / (x0 - x2)) by A4, XCMPLX_1: 89

      .= (((x0 + x1) - (x1 + x2)) / (x0 - x2)) by A4, XCMPLX_1: 89

      .= 1 by A4, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: DIFF_3:44

    (for x holds (f . x) = (x ^2 )) & (x0,x1,x2,x3) are_mutually_distinct implies [!f, x0, x1, x2, x3!] = 0

    proof

      assume that

       A1: for x holds (f . x) = (x ^2 ) and

       A2: (x0,x1,x2,x3) are_mutually_distinct ;

      

       A3: (f . x0) = (x0 ^2 ) & (f . x1) = (x1 ^2 ) & (f . x2) = (x2 ^2 ) & (f . x3) = (x3 ^2 ) by A1;

      

       A4: (x0 - x1) <> 0 & (x1 - x2) <> 0 & (x2 - x3) <> 0 & (x0 - x2) <> 0 & (x1 - x3) <> 0 & (x0 - x3) <> 0 by A2, ZFMISC_1:def 6;

       [!f, x0, x1, x2, x3!] = (((((((x0 - x1) * (x0 + x1)) / (x0 - x1)) - (((x1 - x2) * (x1 + x2)) / (x1 - x2))) / (x0 - x2)) - (((((x1 - x2) * (x1 + x2)) / (x1 - x2)) - (((x2 - x3) * (x2 + x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)) by A3

      .= (((((x0 + x1) - (((x1 - x2) * (x1 + x2)) / (x1 - x2))) / (x0 - x2)) - (((((x1 - x2) * (x1 + x2)) / (x1 - x2)) - (((x2 - x3) * (x2 + x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)) by A4, XCMPLX_1: 89

      .= (((((x0 + x1) - (x1 + x2)) / (x0 - x2)) - (((((x1 - x2) * (x1 + x2)) / (x1 - x2)) - (((x2 - x3) * (x2 + x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)) by A4, XCMPLX_1: 89

      .= (((((x0 + x1) - (x1 + x2)) / (x0 - x2)) - (((x1 + x2) - (((x2 - x3) * (x2 + x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)) by A4, XCMPLX_1: 89

      .= (((((x0 + x1) - (x1 + x2)) / (x0 - x2)) - (((x1 + x2) - (x2 + x3)) / (x1 - x3))) / (x0 - x3)) by A4, XCMPLX_1: 89

      .= ((1 - ((x1 - x3) / (x1 - x3))) / (x0 - x3)) by A4, XCMPLX_1: 60

      .= ((1 - 1) / (x0 - x3)) by A4, XCMPLX_1: 60

      .= 0 ;

      hence thesis;

    end;

    theorem :: DIFF_3:45

    (for x holds (f . x) = (x ^2 )) implies (( fD (f,h)) . x) = (((2 * x) * h) + (h ^2 ))

    proof

      assume

       A1: for x holds (f . x) = (x ^2 );

      then (f . (x + h)) = ((x + h) ^2 );

      

      then (( fD (f,h)) . x) = (((x + h) ^2 ) - (f . x)) by DIFF_1: 3

      .= ((((x ^2 ) + ((2 * x) * h)) + (h ^2 )) - (x ^2 )) by A1

      .= (((2 * x) * h) + (h ^2 ));

      hence thesis;

    end;

    theorem :: DIFF_3:46

    (for x holds (f . x) = (x ^2 )) implies (( bD (f,h)) . x) = (h * ((2 * x) - h))

    proof

      assume

       A1: for x holds (f . x) = (x ^2 );

      then

       A2: (f . (x - h)) = ((x - h) ^2 );

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((x ^2 ) - ((x - h) ^2 )) by A1, A2

      .= (h * ((2 * x) - h));

      hence thesis;

    end;

    theorem :: DIFF_3:47

    (for x holds (f . x) = (x ^2 )) implies (( cD (f,h)) . x) = ((2 * h) * x)

    proof

      assume

       A1: for x holds (f . x) = (x ^2 );

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= (((x + (h / 2)) ^2 ) - (f . (x - (h / 2)))) by A1

      .= (((x + (h / 2)) ^2 ) - ((x - (h / 2)) ^2 )) by A1

      .= (h * (2 * x));

      hence thesis;

    end;

    theorem :: DIFF_3:48

    (for x holds (f . x) = (k / (x ^2 ))) & x0 <> x1 & x0 <> 0 & x1 <> 0 implies [!f, x0, x1!] = ( - ((k / (x0 * x1)) * ((1 / x0) + (1 / x1))))

    proof

      assume that

       A1: for x holds (f . x) = (k / (x ^2 )) and

       A2: x0 <> x1 & x0 <> 0 & x1 <> 0 ;

      

       A3: (x1 - x0) <> 0 by A2;

      (f . x0) = (k / (x0 ^2 )) & (f . x1) = (k / (x1 ^2 )) by A1;

      

      then [!f, x0, x1!] = ((k * ((1 / (x0 ^2 )) - (1 / (x1 ^2 )))) / (x0 - x1))

      .= ((k * (((1 * (x1 ^2 )) - (1 * (x0 ^2 ))) / ((x0 ^2 ) * (x1 ^2 )))) / (x0 - x1)) by A2, XCMPLX_1: 130

      .= (k * ((((x1 - x0) * (x1 + x0)) / ((x0 ^2 ) * (x1 ^2 ))) / ( - (x1 - x0))))

      .= (k * ( - ((((x1 - x0) * (x1 + x0)) / ((x0 ^2 ) * (x1 ^2 ))) / (x1 - x0)))) by XCMPLX_1: 188

      .= ( - (k * ((((x1 - x0) * (x1 + x0)) / (x1 - x0)) / ((x0 ^2 ) * (x1 ^2 )))))

      .= ( - (k * ((x1 + x0) / (((x0 * x0) * x1) * x1)))) by A3, XCMPLX_1: 89

      .= ( - (k * ((x1 / (x1 * ((x0 * x0) * x1))) + (x0 / (x0 * ((x0 * x1) * x1))))))

      .= ( - (k * (((1 / ((x0 * x0) * x1)) * (x1 / x1)) + (x0 / (x0 * ((x0 * x1) * x1)))))) by XCMPLX_1: 103

      .= ( - (k * (((1 / ((x0 * x0) * x1)) * (x1 / x1)) + ((1 / ((x0 * x1) * x1)) * (x0 / x0))))) by XCMPLX_1: 103

      .= ( - (k * (((1 / ((x0 * x0) * x1)) * 1) + ((1 / ((x0 * x1) * x1)) * (x0 / x0))))) by A2, XCMPLX_1: 60

      .= ( - (k * ((1 / (x0 * (x0 * x1))) + (1 / ((x0 * x1) * x1))))) by A2, XCMPLX_1: 60

      .= ( - (k * (((1 / x0) * (1 / (x0 * x1))) + (1 / ((x0 * x1) * x1))))) by XCMPLX_1: 102

      .= ( - (k * (((1 / x0) * (1 / (x0 * x1))) + ((1 / (x0 * x1)) * (1 / x1))))) by XCMPLX_1: 102

      .= ( - ((k / (x0 * x1)) * ((1 / x0) + (1 / x1))));

      hence thesis;

    end;

    theorem :: DIFF_3:49

    (for x holds (f . x) = (k / (x ^2 ))) & x0 <> 0 & x1 <> 0 & x2 <> 0 & (x0,x1,x2) are_mutually_distinct implies [!f, x0, x1, x2!] = ((k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2)))

    proof

      assume that

       A1: for x holds (f . x) = (k / (x ^2 )) and

       A2: x0 <> 0 & x1 <> 0 & x2 <> 0 and

       A3: (x0,x1,x2) are_mutually_distinct ;

      

       A4: (f . x0) = (k / (x0 ^2 )) & (f . x1) = (k / (x1 ^2 )) & (f . x2) = (k / (x2 ^2 )) by A1;

      

       A5: (x1 - x0) <> 0 & (x2 - x1) <> 0 & (x0 - x2) <> 0 by A3, ZFMISC_1:def 5;

       [!f, x0, x1, x2!] = ((((k * ((1 / (x0 ^2 )) - (1 / (x1 ^2 )))) / (x0 - x1)) - ((k * ((1 / (x1 ^2 )) - (1 / (x2 ^2 )))) / (x1 - x2))) / (x0 - x2)) by A4

      .= ((((k * (((1 * (x1 ^2 )) - (1 * (x0 ^2 ))) / ((x0 ^2 ) * (x1 ^2 )))) / (x0 - x1)) - ((k * ((1 / (x1 ^2 )) - (1 / (x2 ^2 )))) / (x1 - x2))) / (x0 - x2)) by A2, XCMPLX_1: 130

      .= ((((k * (((1 * (x1 ^2 )) - (1 * (x0 ^2 ))) / ((x0 ^2 ) * (x1 ^2 )))) / (x0 - x1)) - ((k * (((1 * (x2 ^2 )) - (1 * (x1 ^2 ))) / ((x1 ^2 ) * (x2 ^2 )))) / (x1 - x2))) / (x0 - x2)) by A2, XCMPLX_1: 130

      .= (((k * ((((x1 - x0) * (x1 + x0)) / ((x0 ^2 ) * (x1 ^2 ))) / ( - (x1 - x0)))) - (k * ((((x2 - x1) * (x2 + x1)) / ((x1 ^2 ) * (x2 ^2 ))) / ( - (x2 - x1))))) / (x0 - x2))

      .= (((k * ( - ((((x1 - x0) * (x1 + x0)) / ((x0 ^2 ) * (x1 ^2 ))) / (x1 - x0)))) - (k * ((((x2 - x1) * (x2 + x1)) / ((x1 ^2 ) * (x2 ^2 ))) / ( - (x2 - x1))))) / (x0 - x2)) by XCMPLX_1: 188

      .= ((( - (k * ((((x1 - x0) * (x1 + x0)) / ((x0 ^2 ) * (x1 ^2 ))) / (x1 - x0)))) - (k * ( - ((((x2 - x1) * (x2 + x1)) / ((x1 ^2 ) * (x2 ^2 ))) / (x2 - x1))))) / (x0 - x2)) by XCMPLX_1: 188

      .= ((( - (k * ((((x1 - x0) * (x1 + x0)) / (x1 - x0)) / ((x0 ^2 ) * (x1 ^2 ))))) + (k * ((((x2 - x1) * (x2 + x1)) / (x2 - x1)) / ((x1 ^2 ) * (x2 ^2 ))))) / (x0 - x2))

      .= ((( - (k * ((x1 + x0) / ((x0 ^2 ) * (x1 ^2 ))))) + (k * ((((x2 - x1) * (x2 + x1)) / (x2 - x1)) / ((x1 ^2 ) * (x2 ^2 ))))) / (x0 - x2)) by A5, XCMPLX_1: 89

      .= ((( - (k * ((x1 / (((x0 * x0) * x1) * x1)) + (x0 / (((x0 * x0) * x1) * x1))))) + (k * ((x2 + x1) / (((x1 * x1) * x2) * x2)))) / (x0 - x2)) by A5, XCMPLX_1: 89

      .= ((( - (k * (((1 / ((x0 * x0) * x1)) * (x1 / x1)) + (x0 / (x0 * ((x0 * x1) * x1)))))) + (k * ((x2 / (x2 * ((x1 * x1) * x2))) + (x1 / (x1 * ((x1 * x2) * x2)))))) / (x0 - x2)) by XCMPLX_1: 103

      .= ((( - (k * (((1 / ((x0 * x0) * x1)) * (x1 / x1)) + (x0 / (x0 * ((x0 * x1) * x1)))))) + (k * (((1 / ((x1 * x1) * x2)) * (x2 / x2)) + (x1 / (x1 * ((x1 * x2) * x2)))))) / (x0 - x2)) by XCMPLX_1: 103

      .= ((( - (k * (((1 / ((x0 * x0) * x1)) * (x1 / x1)) + ((1 / ((x0 * x1) * x1)) * (x0 / x0))))) + (k * (((1 / ((x1 * x1) * x2)) * (x2 / x2)) + (x1 / (x1 * ((x1 * x2) * x2)))))) / (x0 - x2)) by XCMPLX_1: 103

      .= ((( - (k * (((1 / ((x0 * x0) * x1)) * (x1 / x1)) + ((1 / ((x0 * x1) * x1)) * (x0 / x0))))) + (k * (((1 / ((x1 * x1) * x2)) * (x2 / x2)) + ((1 / ((x1 * x2) * x2)) * (x1 / x1))))) / (x0 - x2)) by XCMPLX_1: 103

      .= ((( - (k * (((1 / ((x0 * x0) * x1)) * 1) + ((1 / ((x0 * x1) * x1)) * (x0 / x0))))) + (k * (((1 / ((x1 * x1) * x2)) * (x2 / x2)) + ((1 / ((x1 * x2) * x2)) * (x1 / x1))))) / (x0 - x2)) by A2, XCMPLX_1: 60

      .= ((( - (k * (((1 / ((x0 * x0) * x1)) * 1) + ((1 / ((x0 * x1) * x1)) * (x0 / x0))))) + (k * (((1 / ((x1 * x1) * x2)) * 1) + ((1 / ((x1 * x2) * x2)) * (x1 / x1))))) / (x0 - x2)) by A2, XCMPLX_1: 60

      .= ((( - (k * (((1 / ((x0 * x0) * x1)) * 1) + ((1 / ((x0 * x1) * x1)) * 1)))) + (k * (((1 / ((x1 * x1) * x2)) * 1) + ((1 / ((x1 * x2) * x2)) * (x1 / x1))))) / (x0 - x2)) by A2, XCMPLX_1: 60

      .= ((( - (k * ((1 / (x0 * (x0 * x1))) + (1 / ((x0 * x1) * x1))))) + (k * ((1 / (x1 * (x1 * x2))) + (1 / ((x1 * x2) * x2))))) / (x0 - x2)) by A2, XCMPLX_1: 60

      .= ((( - (k * (((1 / x0) * (1 / (x0 * x1))) + (1 / ((x0 * x1) * x1))))) + (k * ((1 / (x1 * (x1 * x2))) + (1 / ((x1 * x2) * x2))))) / (x0 - x2)) by XCMPLX_1: 102

      .= ((( - (k * (((1 / x0) * (1 / (x0 * x1))) + (1 / ((x0 * x1) * x1))))) + (k * (((1 / x1) * (1 / (x1 * x2))) + (1 / ((x1 * x2) * x2))))) / (x0 - x2)) by XCMPLX_1: 102

      .= ((( - (k * (((1 / x0) * (1 / (x0 * x1))) + ((1 / (x0 * x1)) * (1 / x1))))) + (k * (((1 / x1) * (1 / (x1 * x2))) + (1 / ((x1 * x2) * x2))))) / (x0 - x2)) by XCMPLX_1: 102

      .= ((( - ((k * (1 / (x0 * x1))) * ((1 / x0) + (1 / x1)))) + (k * (((1 / x1) * (1 / (x1 * x2))) + ((1 / (x1 * x2)) * (1 / x2))))) / (x0 - x2)) by XCMPLX_1: 102

      .= (k * ((((1 / (x1 * x2)) / (x0 - x2)) * ((1 / x1) + (1 / x2))) - (((1 / (x0 * x1)) / (x0 - x2)) * ((1 / x0) + (1 / x1)))))

      .= (k * (((1 / ((x1 * x2) * (x0 - x2))) * ((1 / x1) + (1 / x2))) - (((1 / (x0 * x1)) / (x0 - x2)) * ((1 / x0) + (1 / x1))))) by XCMPLX_1: 78

      .= (k * (((1 / ((x1 * x2) * (x0 - x2))) * ((1 / x1) + (1 / x2))) - ((1 / ((x0 * x1) * (x0 - x2))) * ((1 / x0) + (1 / x1))))) by XCMPLX_1: 78

      .= (k * (((1 / ((x1 * x2) * (x0 - x2))) * (((1 * x2) + (1 * x1)) / (x1 * x2))) - ((1 / ((x0 * x1) * (x0 - x2))) * ((1 / x0) + (1 / x1))))) by A2, XCMPLX_1: 116

      .= (k * (((1 / ((x1 * x2) * (x0 - x2))) * (((1 * x2) + (1 * x1)) / (x1 * x2))) - ((1 / ((x0 * x1) * (x0 - x2))) * (((1 * x1) + (1 * x0)) / (x0 * x1))))) by A2, XCMPLX_1: 116

      .= (k * (((1 / ((x1 * x2) * (x0 - x2))) / ((x1 * x2) / (x2 + x1))) - ((1 / ((x0 * x1) * (x0 - x2))) * ((x1 + x0) / (x0 * x1))))) by XCMPLX_1: 79

      .= (k * (((1 / ((x1 * x2) * (x0 - x2))) / ((x1 * x2) / (x2 + x1))) - ((1 / ((x0 * x1) * (x0 - x2))) / ((x0 * x1) / (x1 + x0))))) by XCMPLX_1: 79

      .= (k * ((((1 / ((x1 * x2) * (x0 - x2))) / (x1 * x2)) * (x2 + x1)) - ((1 / ((x0 * x1) * (x0 - x2))) / ((x0 * x1) / (x1 + x0))))) by XCMPLX_1: 82

      .= (k * ((((1 / ((x1 * x2) * (x0 - x2))) / (x1 * x2)) * (x2 + x1)) - (((1 / ((x0 * x1) * (x0 - x2))) / (x0 * x1)) * (x1 + x0)))) by XCMPLX_1: 82

      .= (k * ((((x2 + x1) / ((x1 * x2) * (x0 - x2))) / (x1 * x2)) - (((x1 + x0) / ((x0 * x1) * (x0 - x2))) / (x0 * x1))))

      .= (k * (((x2 + x1) / (((x1 * x2) * (x0 - x2)) * (x1 * x2))) - (((x1 + x0) / ((x0 * x1) * (x0 - x2))) / (x0 * x1)))) by XCMPLX_1: 78

      .= (k * (((x2 + x1) / (((x1 * x2) * (x0 - x2)) * (x1 * x2))) - ((x1 + x0) / (((x0 * x1) * (x0 - x2)) * (x0 * x1))))) by XCMPLX_1: 78

      .= (k * (((x2 + x1) / (((x1 ^2 ) * (x0 - x2)) * (x2 ^2 ))) - ((x1 + x0) / (((x1 ^2 ) * (x0 - x2)) * (x0 ^2 )))))

      .= (k * ((((x2 + x1) / ((x1 ^2 ) * (x0 - x2))) / (x2 ^2 )) - ((x1 + x0) / (((x1 ^2 ) * (x0 - x2)) * (x0 ^2 ))))) by XCMPLX_1: 78

      .= (k * (((1 / ((x1 ^2 ) * (x0 - x2))) * ((x2 + x1) / (x2 ^2 ))) - (((x1 + x0) / ((x1 ^2 ) * (x0 - x2))) / (x0 ^2 )))) by XCMPLX_1: 78

      .= (k * ((1 / ((x1 ^2 ) * (x0 - x2))) * (((x2 + x1) / (x2 ^2 )) - ((x1 + x0) / (x0 ^2 )))))

      .= (k * ((1 / ((x1 ^2 ) * (x0 - x2))) * ((((x2 + x1) * (x0 ^2 )) - ((x1 + x0) * (x2 ^2 ))) / ((x2 ^2 ) * (x0 ^2 ))))) by A2, XCMPLX_1: 130

      .= (k * ((((1 * (x0 - x2)) / ((x1 ^2 ) * (x0 - x2))) * ((x1 * (x0 + x2)) + (x0 * x2))) / ((x2 ^2 ) * (x0 ^2 ))))

      .= (k * (((1 / (x1 ^2 )) * (((x1 * x0) + (x1 * x2)) + (x0 * x2))) / ((x2 ^2 ) * (x0 ^2 )))) by A5, XCMPLX_1: 91

      .= (k * (((((x1 * x0) + (x1 * x2)) + (x0 * x2)) / (x1 ^2 )) / ((x2 ^2 ) * (x0 ^2 ))))

      .= (k * ((((x1 * x0) + (x1 * x2)) + (x0 * x2)) / ((x1 ^2 ) * ((x2 ^2 ) * (x0 ^2 ))))) by XCMPLX_1: 78

      .= (k * ((((1 * (x1 * x0)) / (((x1 * (x2 ^2 )) * x0) * (x1 * x0))) + ((1 * (x1 * x2)) / (((x1 * x2) * (x0 ^2 )) * (x1 * x2)))) + ((1 * (x0 * x2)) / ((((x1 ^2 ) * x2) * x0) * (x0 * x2)))))

      .= (k * (((1 / ((x1 * (x2 ^2 )) * x0)) + ((1 * (x1 * x2)) / (((x1 * x2) * (x0 ^2 )) * (x1 * x2)))) + ((1 * (x0 * x2)) / ((((x1 ^2 ) * x2) * x0) * (x0 * x2))))) by A2, XCMPLX_1: 91

      .= (k * (((1 / ((x1 * (x2 ^2 )) * x0)) + (1 / ((x1 * x2) * (x0 ^2 )))) + ((1 * (x0 * x2)) / ((((x1 ^2 ) * x2) * x0) * (x0 * x2))))) by A2, XCMPLX_1: 91

      .= (k * (((1 / (((x1 * x2) * x0) * x2)) + (1 / (((x1 * x2) * x0) * x0))) + (1 / (((x1 * x2) * x0) * x1)))) by A2, XCMPLX_1: 91

      .= (k * ((((1 / ((x1 * x2) * x0)) * (1 / x2)) + (1 / (((x1 * x2) * x0) * x0))) + (1 / (((x1 * x2) * x0) * x1)))) by XCMPLX_1: 102

      .= (k * ((((1 / ((x1 * x2) * x0)) * (1 / x2)) + ((1 / ((x1 * x2) * x0)) * (1 / x0))) + (1 / (((x1 * x2) * x0) * x1)))) by XCMPLX_1: 102

      .= (k * ((((1 / ((x1 * x2) * x0)) * (1 / x2)) + ((1 / ((x1 * x2) * x0)) * (1 / x0))) + ((1 / ((x1 * x2) * x0)) * (1 / x1)))) by XCMPLX_1: 102

      .= ((k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2)));

      hence thesis;

    end;

    theorem :: DIFF_3:50

    (for x holds (f . x) = (k / (x ^2 ))) & x <> 0 & (x + h) <> 0 implies (( fD (f,h)) . x) = (((( - k) * h) * ((2 * x) + h)) / (((x ^2 ) + (h * x)) ^2 ))

    proof

      assume that

       A1: for x holds (f . x) = (k / (x ^2 )) and

       A2: x <> 0 & (x + h) <> 0 ;

      (( fD (f,h)) . x) = ((f . (x + h)) - (f . x)) by DIFF_1: 3

      .= ((k / ((x + h) ^2 )) - (f . x)) by A1

      .= ((k / ((x + h) ^2 )) - (k / (x ^2 ))) by A1

      .= (((k * (x ^2 )) - (k * ((x + h) ^2 ))) / (((x + h) ^2 ) * (x ^2 ))) by A2, XCMPLX_1: 130

      .= (((( - k) * h) * ((2 * x) + h)) / (((x ^2 ) + (h * x)) ^2 ));

      hence thesis;

    end;

    theorem :: DIFF_3:51

    (for x holds (f . x) = (k / (x ^2 ))) & x <> 0 & (x - h) <> 0 implies (( bD (f,h)) . x) = (((( - k) * h) * ((2 * x) - h)) / (((x ^2 ) - (x * h)) ^2 ))

    proof

      assume that

       A1: for x holds (f . x) = (k / (x ^2 )) and

       A2: x <> 0 & (x - h) <> 0 ;

      

       A3: (f . (x - h)) = (k / ((x - h) ^2 )) by A1;

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((k / (x ^2 )) - (k / ((x - h) ^2 ))) by A1, A3

      .= (((k * ((x - h) ^2 )) - (k * (x ^2 ))) / ((x ^2 ) * ((x - h) ^2 ))) by A2, XCMPLX_1: 130

      .= (((( - k) * h) * ((2 * x) - h)) / (((x ^2 ) - (x * h)) ^2 ));

      hence thesis;

    end;

    theorem :: DIFF_3:52

    (for x holds (f . x) = (k / (x ^2 ))) & (x + (h / 2)) <> 0 & (x - (h / 2)) <> 0 implies (( cD (f,h)) . x) = (( - (((2 * h) * k) * x)) / (((x ^2 ) - ((h / 2) ^2 )) ^2 ))

    proof

      assume that

       A1: for x holds (f . x) = (k / (x ^2 )) and

       A2: (x + (h / 2)) <> 0 & (x - (h / 2)) <> 0 ;

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= ((k / ((x + (h / 2)) ^2 )) - (f . (x - (h / 2)))) by A1

      .= ((k / ((x + (h / 2)) ^2 )) - (k / ((x - (h / 2)) ^2 ))) by A1

      .= (((k * ((x - (h / 2)) ^2 )) - (k * ((x + (h / 2)) ^2 ))) / (((x + (h / 2)) ^2 ) * ((x - (h / 2)) ^2 ))) by A2, XCMPLX_1: 130

      .= (( - (((2 * h) * k) * x)) / (((x ^2 ) - ((h / 2) ^2 )) ^2 ));

      hence thesis;

    end;

    theorem :: DIFF_3:53

     [!(( sin (#) sin ) (#) sin ), x0, x1!] = (((1 / 2) * (((3 * ( cos ((x0 + x1) / 2))) * ( sin ((x0 - x1) / 2))) - (( cos ((3 * (x0 + x1)) / 2)) * ( sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1))

    proof

      set y = (3 * x0);

      set z = (3 * x1);

       [!(( sin (#) sin ) (#) sin ), x0, x1!] = ((((( sin (#) sin ) . x0) * ( sin . x0)) - ((( sin (#) sin ) (#) sin ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( sin . x0) * ( sin . x0)) * ( sin . x0)) - ((( sin (#) sin ) (#) sin ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( sin . x0) * ( sin . x0)) * ( sin . x0)) - ((( sin (#) sin ) . x1) * ( sin . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( sin x0) * ( sin x0)) * ( sin x0)) - ((( sin x1) * ( sin x1)) * ( sin x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((1 / 4) * (((( sin ((x0 + x0) - x0)) + ( sin ((x0 + x0) - x0))) + ( sin ((x0 + x0) - x0))) - ( sin ((x0 + x0) + x0)))) - ((( sin x1) * ( sin x1)) * ( sin x1))) / (x0 - x1)) by SIN_COS4: 33

      .= ((((1 / 4) * ((3 * ( sin x0)) - ( sin (3 * x0)))) - ((1 / 4) * (((( sin ((x1 + x1) - x1)) + ( sin ((x1 + x1) - x1))) + ( sin ((x1 + x1) - x1))) - ( sin ((x1 + x1) + x1))))) / (x0 - x1)) by SIN_COS4: 33

      .= (((1 / 4) * ((3 * (( sin x0) - ( sin x1))) - (( sin y) - ( sin z)))) / (x0 - x1))

      .= (((1 / 4) * ((3 * (2 * (( cos ((x0 + x1) / 2)) * ( sin ((x0 - x1) / 2))))) - (( sin y) - ( sin z)))) / (x0 - x1)) by SIN_COS4: 16

      .= (((1 / 4) * ((3 * (2 * (( cos ((x0 + x1) / 2)) * ( sin ((x0 - x1) / 2))))) - (2 * (( cos ((y + z) / 2)) * ( sin ((y - z) / 2)))))) / (x0 - x1)) by SIN_COS4: 16

      .= (((1 / 2) * (((3 * ( cos ((x0 + x1) / 2))) * ( sin ((x0 - x1) / 2))) - (( cos ((3 * (x0 + x1)) / 2)) * ( sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1));

      hence thesis;

    end;

    theorem :: DIFF_3:54

    (( fD ((( sin (#) sin ) (#) sin ),h)) . x) = ((1 / 2) * (((3 * ( cos (((2 * x) + h) / 2))) * ( sin (h / 2))) - (( cos ((3 * ((2 * x) + h)) / 2)) * ( sin ((3 * h) / 2)))))

    proof

      (( fD ((( sin (#) sin ) (#) sin ),h)) . x) = (((( sin (#) sin ) (#) sin ) . (x + h)) - ((( sin (#) sin ) (#) sin ) . x)) by DIFF_1: 3

      .= (((( sin (#) sin ) . (x + h)) * ( sin . (x + h))) - ((( sin (#) sin ) (#) sin ) . x)) by VALUED_1: 5

      .= (((( sin . (x + h)) * ( sin . (x + h))) * ( sin . (x + h))) - ((( sin (#) sin ) (#) sin ) . x)) by VALUED_1: 5

      .= (((( sin . (x + h)) * ( sin . (x + h))) * ( sin . (x + h))) - ((( sin (#) sin ) . x) * ( sin . x))) by VALUED_1: 5

      .= (((( sin (x + h)) * ( sin (x + h))) * ( sin (x + h))) - ((( sin x) * ( sin x)) * ( sin x))) by VALUED_1: 5

      .= (((1 / 4) * (((( sin (((x + h) + (x + h)) - (x + h))) + ( sin (((x + h) + (x + h)) - (x + h)))) + ( sin (((x + h) + (x + h)) - (x + h)))) - ( sin (((x + h) + (x + h)) + (x + h))))) - ((( sin x) * ( sin x)) * ( sin x))) by SIN_COS4: 33

      .= (((1 / 4) * (((( sin (x + h)) + ( sin (x + h))) + ( sin (x + h))) - ( sin (3 * (x + h))))) - ((1 / 4) * (((( sin ((x + x) - x)) + ( sin ((x + x) - x))) + ( sin ((x + x) - x))) - ( sin ((x + x) + x))))) by SIN_COS4: 33

      .= ((1 / 4) * ((3 * (( sin (x + h)) - ( sin x))) - (( sin (3 * (x + h))) - ( sin (3 * x)))))

      .= ((1 / 4) * ((3 * (2 * (( cos (((x + h) + x) / 2)) * ( sin (((x + h) - x) / 2))))) - (( sin (3 * (x + h))) - ( sin (3 * x))))) by SIN_COS4: 16

      .= ((1 / 4) * ((3 * (2 * (( cos (((x + h) + x) / 2)) * ( sin (((x + h) - x) / 2))))) - (2 * (( cos (((3 * (x + h)) + (3 * x)) / 2)) * ( sin (((3 * (x + h)) - (3 * x)) / 2)))))) by SIN_COS4: 16

      .= ((1 / 2) * (((3 * ( cos (((2 * x) + h) / 2))) * ( sin (h / 2))) - (( cos ((3 * ((2 * x) + h)) / 2)) * ( sin ((3 * h) / 2)))));

      hence thesis;

    end;

    theorem :: DIFF_3:55

    (( bD ((( sin (#) sin ) (#) sin ),h)) . x) = ((1 / 2) * (((3 * ( cos (((2 * x) - h) / 2))) * ( sin (h / 2))) - (( cos ((3 * ((2 * x) - h)) / 2)) * ( sin ((3 * h) / 2)))))

    proof

      (( bD ((( sin (#) sin ) (#) sin ),h)) . x) = (((( sin (#) sin ) (#) sin ) . x) - ((( sin (#) sin ) (#) sin ) . (x - h))) by DIFF_1: 4

      .= (((( sin (#) sin ) . x) * ( sin . x)) - ((( sin (#) sin ) (#) sin ) . (x - h))) by VALUED_1: 5

      .= (((( sin . x) * ( sin . x)) * ( sin . x)) - ((( sin (#) sin ) (#) sin ) . (x - h))) by VALUED_1: 5

      .= (((( sin . x) * ( sin . x)) * ( sin . x)) - ((( sin (#) sin ) . (x - h)) * ( sin . (x - h)))) by VALUED_1: 5

      .= (((( sin x) * ( sin x)) * ( sin x)) - ((( sin (x - h)) * ( sin (x - h))) * ( sin (x - h)))) by VALUED_1: 5

      .= (((1 / 4) * (((( sin ((x + x) - x)) + ( sin ((x + x) - x))) + ( sin ((x + x) - x))) - ( sin ((x + x) + x)))) - ((( sin (x - h)) * ( sin (x - h))) * ( sin (x - h)))) by SIN_COS4: 33

      .= (((1 / 4) * (((( sin x) + ( sin x)) + ( sin x)) - ( sin (3 * x)))) - ((1 / 4) * (((( sin (((x - h) + (x - h)) - (x - h))) + ( sin (((x - h) + (x - h)) - (x - h)))) + ( sin (((x - h) + (x - h)) - (x - h)))) - ( sin (((x - h) + (x - h)) + (x - h)))))) by SIN_COS4: 33

      .= ((1 / 4) * ((3 * (( sin x) - ( sin (x - h)))) - (( sin (3 * x)) - ( sin (3 * (x - h))))))

      .= ((1 / 4) * ((3 * (2 * (( cos ((x + (x - h)) / 2)) * ( sin ((x - (x - h)) / 2))))) - (( sin (3 * x)) - ( sin (3 * (x - h)))))) by SIN_COS4: 16

      .= ((1 / 4) * ((3 * (2 * (( cos (((2 * x) - h) / 2)) * ( sin (h / 2))))) - (2 * (( cos (((3 * x) + (3 * (x - h))) / 2)) * ( sin (((3 * x) - (3 * (x - h))) / 2)))))) by SIN_COS4: 16

      .= ((1 / 2) * (((3 * ( cos (((2 * x) - h) / 2))) * ( sin (h / 2))) - (( cos ((3 * ((2 * x) - h)) / 2)) * ( sin ((3 * h) / 2)))));

      hence thesis;

    end;

    theorem :: DIFF_3:56

    (( cD ((( sin (#) sin ) (#) sin ),h)) . x) = ((1 / 2) * (((3 * ( cos x)) * ( sin (h / 2))) - (( cos (3 * x)) * ( sin ((3 * h) / 2)))))

    proof

      (( cD ((( sin (#) sin ) (#) sin ),h)) . x) = (((( sin (#) sin ) (#) sin ) . (x + (h / 2))) - ((( sin (#) sin ) (#) sin ) . (x - (h / 2)))) by DIFF_1: 5

      .= (((( sin (#) sin ) . (x + (h / 2))) * ( sin . (x + (h / 2)))) - ((( sin (#) sin ) (#) sin ) . (x - (h / 2)))) by VALUED_1: 5

      .= (((( sin . (x + (h / 2))) * ( sin . (x + (h / 2)))) * ( sin . (x + (h / 2)))) - ((( sin (#) sin ) (#) sin ) . (x - (h / 2)))) by VALUED_1: 5

      .= (((( sin . (x + (h / 2))) * ( sin . (x + (h / 2)))) * ( sin . (x + (h / 2)))) - ((( sin (#) sin ) . (x - (h / 2))) * ( sin . (x - (h / 2))))) by VALUED_1: 5

      .= (((( sin (x + (h / 2))) * ( sin (x + (h / 2)))) * ( sin (x + (h / 2)))) - ((( sin (x - (h / 2))) * ( sin (x - (h / 2)))) * ( sin (x - (h / 2))))) by VALUED_1: 5

      .= (((1 / 4) * (((( sin (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2)))) + ( sin (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + ( sin (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) - ( sin (((x + (h / 2)) + (x + (h / 2))) + (x + (h / 2)))))) - ((( sin (x - (h / 2))) * ( sin (x - (h / 2)))) * ( sin (x - (h / 2))))) by SIN_COS4: 33

      .= (((1 / 4) * (((( sin (x + (h / 2))) + ( sin (x + (h / 2)))) + ( sin (x + (h / 2)))) - ( sin (3 * (x + (h / 2)))))) - ((1 / 4) * (((( sin (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2)))) + ( sin (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + ( sin (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) - ( sin (((x - (h / 2)) + (x - (h / 2))) + (x - (h / 2))))))) by SIN_COS4: 33

      .= ((1 / 4) * ((3 * (( sin (x + (h / 2))) - ( sin (x - (h / 2))))) - (( sin (3 * (x + (h / 2)))) - ( sin (3 * (x - (h / 2)))))))

      .= ((1 / 4) * ((3 * (2 * (( cos (((x + (h / 2)) + (x - (h / 2))) / 2)) * ( sin (((x + (h / 2)) - (x - (h / 2))) / 2))))) - (( sin (3 * (x + (h / 2)))) - ( sin (3 * (x - (h / 2))))))) by SIN_COS4: 16

      .= ((1 / 4) * ((3 * (2 * (( cos ((2 * x) / 2)) * ( sin (h / 2))))) - (2 * (( cos (((3 * (x + (h / 2))) + (3 * (x - (h / 2)))) / 2)) * ( sin (((3 * (x + (h / 2))) - (3 * (x - (h / 2)))) / 2)))))) by SIN_COS4: 16

      .= ((1 / 2) * (((3 * ( cos x)) * ( sin (h / 2))) - (( cos (3 * x)) * ( sin ((3 * h) / 2)))));

      hence thesis;

    end;

    theorem :: DIFF_3:57

     [!(( cos (#) cos ) (#) cos ), x0, x1!] = ( - (((1 / 2) * (((3 * ( sin ((x0 + x1) / 2))) * ( sin ((x0 - x1) / 2))) + (( sin (((3 * x0) + (3 * x1)) / 2)) * ( sin (((3 * x0) - (3 * x1)) / 2))))) / (x0 - x1)))

    proof

       [!(( cos (#) cos ) (#) cos ), x0, x1!] = ((((( cos (#) cos ) . x0) * ( cos . x0)) - ((( cos (#) cos ) (#) cos ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cos . x0) * ( cos . x0)) * ( cos . x0)) - ((( cos (#) cos ) (#) cos ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cos . x0) * ( cos . x0)) * ( cos . x0)) - ((( cos (#) cos ) . x1) * ( cos . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cos x0) * ( cos x0)) * ( cos x0)) - ((( cos x1) * ( cos x1)) * ( cos x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((1 / 4) * (((( cos ((x0 + x0) - x0)) + ( cos ((x0 + x0) - x0))) + ( cos ((x0 + x0) - x0))) + ( cos ((x0 + x0) + x0)))) - ((( cos x1) * ( cos x1)) * ( cos x1))) / (x0 - x1)) by SIN_COS4: 36

      .= ((((1 / 4) * (((( cos x0) + ( cos x0)) + ( cos x0)) + ( cos (3 * x0)))) - ((1 / 4) * (((( cos ((x1 + x1) - x1)) + ( cos ((x1 + x1) - x1))) + ( cos ((x1 + x1) - x1))) + ( cos ((x1 + x1) + x1))))) / (x0 - x1)) by SIN_COS4: 36

      .= (((1 / 4) * ((3 * (( cos x0) - ( cos x1))) + (( cos (3 * x0)) - ( cos (3 * x1))))) / (x0 - x1))

      .= (((1 / 4) * ((3 * ( - (2 * (( sin ((x0 + x1) / 2)) * ( sin ((x0 - x1) / 2)))))) + (( cos (3 * x0)) - ( cos (3 * x1))))) / (x0 - x1)) by SIN_COS4: 18

      .= (((1 / 4) * (((3 * ( - 2)) * (( sin ((x0 + x1) / 2)) * ( sin ((x0 - x1) / 2)))) + ( - (2 * (( sin (((3 * x0) + (3 * x1)) / 2)) * ( sin (((3 * x0) - (3 * x1)) / 2))))))) / (x0 - x1)) by SIN_COS4: 18

      .= (( - ((1 / 2) * (((3 * ( sin ((x0 + x1) / 2))) * ( sin ((x0 - x1) / 2))) + (( sin (((3 * x0) + (3 * x1)) / 2)) * ( sin (((3 * x0) - (3 * x1)) / 2)))))) / (x0 - x1));

      hence thesis;

    end;

    theorem :: DIFF_3:58

    (( fD ((( cos (#) cos ) (#) cos ),h)) . x) = ( - ((1 / 2) * (((3 * ( sin (((2 * x) + h) / 2))) * ( sin (h / 2))) + (( sin ((3 * ((2 * x) + h)) / 2)) * ( sin ((3 * h) / 2))))))

    proof

      (( fD ((( cos (#) cos ) (#) cos ),h)) . x) = (((( cos (#) cos ) (#) cos ) . (x + h)) - ((( cos (#) cos ) (#) cos ) . x)) by DIFF_1: 3

      .= (((( cos (#) cos ) . (x + h)) * ( cos . (x + h))) - ((( cos (#) cos ) (#) cos ) . x)) by VALUED_1: 5

      .= (((( cos . (x + h)) * ( cos . (x + h))) * ( cos . (x + h))) - ((( cos (#) cos ) (#) cos ) . x)) by VALUED_1: 5

      .= (((( cos . (x + h)) * ( cos . (x + h))) * ( cos . (x + h))) - ((( cos (#) cos ) . x) * ( cos . x))) by VALUED_1: 5

      .= (((( cos (x + h)) * ( cos (x + h))) * ( cos (x + h))) - ((( cos x) * ( cos x)) * ( cos x))) by VALUED_1: 5

      .= (((1 / 4) * (((( cos (((x + h) + (x + h)) - (x + h))) + ( cos (((x + h) + (x + h)) - (x + h)))) + ( cos (((x + h) + (x + h)) - (x + h)))) + ( cos (((x + h) + (x + h)) + (x + h))))) - ((( cos x) * ( cos x)) * ( cos x))) by SIN_COS4: 36

      .= (((1 / 4) * (((( cos (x + h)) + ( cos (x + h))) + ( cos (x + h))) + ( cos (3 * (x + h))))) - ((1 / 4) * (((( cos ((x + x) - x)) + ( cos ((x + x) - x))) + ( cos ((x + x) - x))) + ( cos ((x + x) + x))))) by SIN_COS4: 36

      .= ((1 / 4) * ((3 * (( cos (x + h)) - ( cos x))) + (( cos (3 * (x + h))) - ( cos (3 * x)))))

      .= ((1 / 4) * ((3 * ( - (2 * (( sin (((x + h) + x) / 2)) * ( sin (((x + h) - x) / 2)))))) + (( cos (3 * (x + h))) - ( cos (3 * x))))) by SIN_COS4: 18

      .= ((1 / 4) * ((3 * ( - (2 * (( sin (((2 * x) + h) / 2)) * ( sin (h / 2)))))) + ( - (2 * (( sin (((3 * (x + h)) + (3 * x)) / 2)) * ( sin (((3 * (x + h)) - (3 * x)) / 2))))))) by SIN_COS4: 18

      .= (( - (1 / 2)) * (((3 * ( sin (((2 * x) + h) / 2))) * ( sin (h / 2))) + (( sin ((3 * ((2 * x) + h)) / 2)) * ( sin ((3 * h) / 2)))));

      hence thesis;

    end;

    theorem :: DIFF_3:59

    (( bD ((( cos (#) cos ) (#) cos ),h)) . x) = ( - ((1 / 2) * (((3 * ( sin (((2 * x) - h) / 2))) * ( sin (h / 2))) + (( sin ((3 * ((2 * x) - h)) / 2)) * ( sin ((3 * h) / 2))))))

    proof

      (( bD ((( cos (#) cos ) (#) cos ),h)) . x) = (((( cos (#) cos ) (#) cos ) . x) - ((( cos (#) cos ) (#) cos ) . (x - h))) by DIFF_1: 4

      .= (((( cos (#) cos ) . x) * ( cos . x)) - ((( cos (#) cos ) (#) cos ) . (x - h))) by VALUED_1: 5

      .= (((( cos . x) * ( cos . x)) * ( cos . x)) - ((( cos (#) cos ) (#) cos ) . (x - h))) by VALUED_1: 5

      .= (((( cos . x) * ( cos . x)) * ( cos . x)) - ((( cos (#) cos ) . (x - h)) * ( cos . (x - h)))) by VALUED_1: 5

      .= (((( cos x) * ( cos x)) * ( cos x)) - ((( cos (x - h)) * ( cos (x - h))) * ( cos (x - h)))) by VALUED_1: 5

      .= (((1 / 4) * (((( cos ((x + x) - x)) + ( cos ((x + x) - x))) + ( cos ((x + x) - x))) + ( cos ((x + x) + x)))) - ((( cos (x - h)) * ( cos (x - h))) * ( cos (x - h)))) by SIN_COS4: 36

      .= (((1 / 4) * (((( cos x) + ( cos x)) + ( cos x)) + ( cos (3 * x)))) - ((1 / 4) * (((( cos (((x - h) + (x - h)) - (x - h))) + ( cos (((x - h) + (x - h)) - (x - h)))) + ( cos (((x - h) + (x - h)) - (x - h)))) + ( cos (((x - h) + (x - h)) + (x - h)))))) by SIN_COS4: 36

      .= ((1 / 4) * ((3 * (( cos x) - ( cos (x - h)))) + (( cos (3 * x)) - ( cos (3 * (x - h))))))

      .= ((1 / 4) * ((3 * ( - (2 * (( sin ((x + (x - h)) / 2)) * ( sin ((x - (x - h)) / 2)))))) + (( cos (3 * x)) - ( cos (3 * (x - h)))))) by SIN_COS4: 18

      .= ((1 / 4) * ((3 * ( - (2 * (( sin (((2 * x) - h) / 2)) * ( sin (h / 2)))))) + ( - (2 * (( sin (((3 * x) + (3 * (x - h))) / 2)) * ( sin (((3 * x) - (3 * (x - h))) / 2))))))) by SIN_COS4: 18

      .= (( - (1 / 2)) * ((3 * (( sin (((2 * x) - h) / 2)) * ( sin (h / 2)))) + (( sin ((3 * ((2 * x) - h)) / 2)) * ( sin ((3 * h) / 2)))));

      hence thesis;

    end;

    theorem :: DIFF_3:60

    (( cD ((( cos (#) cos ) (#) cos ),h)) . x) = ( - ((1 / 2) * (((3 * ( sin x)) * ( sin (h / 2))) + (( sin (3 * x)) * ( sin ((3 * h) / 2))))))

    proof

      (( cD ((( cos (#) cos ) (#) cos ),h)) . x) = (((( cos (#) cos ) (#) cos ) . (x + (h / 2))) - ((( cos (#) cos ) (#) cos ) . (x - (h / 2)))) by DIFF_1: 5

      .= (((( cos (#) cos ) . (x + (h / 2))) * ( cos . (x + (h / 2)))) - ((( cos (#) cos ) (#) cos ) . (x - (h / 2)))) by VALUED_1: 5

      .= (((( cos . (x + (h / 2))) * ( cos . (x + (h / 2)))) * ( cos . (x + (h / 2)))) - ((( cos (#) cos ) (#) cos ) . (x - (h / 2)))) by VALUED_1: 5

      .= (((( cos . (x + (h / 2))) * ( cos . (x + (h / 2)))) * ( cos . (x + (h / 2)))) - ((( cos (#) cos ) . (x - (h / 2))) * ( cos . (x - (h / 2))))) by VALUED_1: 5

      .= (((( cos (x + (h / 2))) * ( cos (x + (h / 2)))) * ( cos (x + (h / 2)))) - ((( cos (x - (h / 2))) * ( cos (x - (h / 2)))) * ( cos (x - (h / 2))))) by VALUED_1: 5

      .= (((1 / 4) * (((( cos (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2)))) + ( cos (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + ( cos (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + ( cos (((x + (h / 2)) + (x + (h / 2))) + (x + (h / 2)))))) - ((( cos (x - (h / 2))) * ( cos (x - (h / 2)))) * ( cos (x - (h / 2))))) by SIN_COS4: 36

      .= (((1 / 4) * (((( cos (x + (h / 2))) + ( cos (x + (h / 2)))) + ( cos (x + (h / 2)))) + ( cos (3 * (x + (h / 2)))))) - ((1 / 4) * (((( cos (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2)))) + ( cos (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + ( cos (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + ( cos (((x - (h / 2)) + (x - (h / 2))) + (x - (h / 2))))))) by SIN_COS4: 36

      .= ((1 / 4) * ((3 * (( cos (x + (h / 2))) - ( cos (x - (h / 2))))) + (( cos (3 * (x + (h / 2)))) - ( cos (3 * (x - (h / 2)))))))

      .= ((1 / 4) * ((3 * ( - (2 * (( sin (((x + (h / 2)) + (x - (h / 2))) / 2)) * ( sin (((x + (h / 2)) - (x - (h / 2))) / 2)))))) + (( cos (3 * (x + (h / 2)))) - ( cos (3 * (x - (h / 2))))))) by SIN_COS4: 18

      .= ((1 / 4) * ((3 * ( - (2 * (( sin ((2 * x) / 2)) * ( sin (h / 2)))))) + ( - (2 * (( sin (((3 * (x + (h / 2))) + (3 * (x - (h / 2)))) / 2)) * ( sin (((3 * (x + (h / 2))) - (3 * (x - (h / 2)))) / 2))))))) by SIN_COS4: 18

      .= ( - ((1 / 2) * ((3 * (( sin x) * ( sin (h / 2)))) + (( sin (3 * x)) * ( sin ((3 * h) / 2))))));

      hence thesis;

    end;

    theorem :: DIFF_3:61

    (for x holds (f . x) = (1 / ( sin x))) & ( sin x0) <> 0 & ( sin x1) <> 0 implies [!f, x0, x1!] = ( - (((2 * (( sin x1) - ( sin x0))) / (( cos (x0 + x1)) - ( cos (x0 - x1)))) / (x0 - x1)))

    proof

      assume that

       A1: for x holds (f . x) = (1 / ( sin x)) and

       A2: ( sin x0) <> 0 & ( sin x1) <> 0 ;

      (f . x0) = (1 / ( sin x0)) & (f . x1) = (1 / ( sin x1)) by A1;

      

      then [!f, x0, x1!] = ((((1 * ( sin x1)) - (1 * ( sin x0))) / (( sin x0) * ( sin x1))) / (x0 - x1)) by A2, XCMPLX_1: 130

      .= (((( sin x1) - ( sin x0)) / ( - ((1 / 2) * (( cos (x0 + x1)) - ( cos (x0 - x1)))))) / (x0 - x1)) by SIN_COS4: 29

      .= (((( sin x1) - ( sin x0)) / (( - (1 / 2)) * (( cos (x0 + x1)) - ( cos (x0 - x1))))) / (x0 - x1))

      .= ((((( sin x1) - ( sin x0)) / ( - (1 / 2))) / (( cos (x0 + x1)) - ( cos (x0 - x1)))) / (x0 - x1)) by XCMPLX_1: 78

      .= (((( - 2) * (( sin x1) - ( sin x0))) / (( cos (x0 + x1)) - ( cos (x0 - x1)))) / (x0 - x1));

      hence thesis;

    end;

    theorem :: DIFF_3:62

    (for x holds (f . x) = (1 / ( sin x))) & ( sin x) <> 0 & ( sin (x + h)) <> 0 implies (( fD (f,h)) . x) = ( - ((2 * (( sin x) - ( sin (x + h)))) / (( cos ((2 * x) + h)) - ( cos h))))

    proof

      assume that

       A1: for x holds (f . x) = (1 / ( sin x)) and

       A2: ( sin x) <> 0 & ( sin (x + h)) <> 0 ;

      (f . (x + h)) = (1 / ( sin (x + h))) by A1;

      

      then (( fD (f,h)) . x) = ((1 / ( sin (x + h))) - (f . x)) by DIFF_1: 3

      .= ((1 / ( sin (x + h))) - (1 / ( sin x))) by A1

      .= (((1 * ( sin x)) - (1 * ( sin (x + h)))) / (( sin (x + h)) * ( sin x))) by A2, XCMPLX_1: 130

      .= ((( sin x) - ( sin (x + h))) / ( - ((1 / 2) * (( cos ((x + h) + x)) - ( cos ((x + h) - x)))))) by SIN_COS4: 29

      .= ((( sin x) - ( sin (x + h))) / (( - (1 / 2)) * (( cos ((x + h) + x)) - ( cos ((x + h) - x)))))

      .= (((( sin x) - ( sin (x + h))) / ( - (1 / 2))) / (( cos ((2 * x) + h)) - ( cos h))) by XCMPLX_1: 78

      .= (( - 2) * ((( sin x) - ( sin (x + h))) / (( cos ((2 * x) + h)) - ( cos h))));

      hence thesis;

    end;

    theorem :: DIFF_3:63

    (for x holds (f . x) = (1 / ( sin x))) & ( sin x) <> 0 & ( sin (x - h)) <> 0 implies (( bD (f,h)) . x) = ((( - 2) * (( sin (x - h)) - ( sin x))) / (( cos ((2 * x) - h)) - ( cos h)))

    proof

      assume that

       A1: for x holds (f . x) = (1 / ( sin x)) and

       A2: ( sin x) <> 0 & ( sin (x - h)) <> 0 ;

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((1 / ( sin x)) - (f . (x - h))) by A1

      .= ((1 / ( sin x)) - (1 / ( sin (x - h)))) by A1

      .= (((1 * ( sin (x - h))) - (1 * ( sin x))) / (( sin x) * ( sin (x - h)))) by A2, XCMPLX_1: 130

      .= ((( sin (x - h)) - ( sin x)) / ( - ((1 / 2) * (( cos (x + (x - h))) - ( cos (x - (x - h))))))) by SIN_COS4: 29

      .= ((( sin (x - h)) - ( sin x)) / (( - (1 / 2)) * (( cos ((2 * x) - h)) - ( cos h))))

      .= (((( sin (x - h)) - ( sin x)) / ( - (1 / 2))) / (( cos ((2 * x) - h)) - ( cos h))) by XCMPLX_1: 78

      .= (( - 2) * ((( sin (x - h)) - ( sin x)) / (( cos ((2 * x) - h)) - ( cos h))));

      hence thesis;

    end;

    theorem :: DIFF_3:64

    (for x holds (f . x) = (1 / ( sin x))) & ( sin (x + (h / 2))) <> 0 & ( sin (x - (h / 2))) <> 0 implies (( cD (f,h)) . x) = ( - ((2 * (( sin (x - (h / 2))) - ( sin (x + (h / 2))))) / (( cos (2 * x)) - ( cos h))))

    proof

      assume that

       A1: for x holds (f . x) = (1 / ( sin x)) and

       A2: ( sin (x + (h / 2))) <> 0 & ( sin (x - (h / 2))) <> 0 ;

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= ((1 / ( sin (x + (h / 2)))) - (f . (x - (h / 2)))) by A1

      .= ((1 / ( sin (x + (h / 2)))) - (1 / ( sin (x - (h / 2))))) by A1

      .= (((1 * ( sin (x - (h / 2)))) - (1 * ( sin (x + (h / 2))))) / (( sin (x + (h / 2))) * ( sin (x - (h / 2))))) by A2, XCMPLX_1: 130

      .= ((( sin (x - (h / 2))) - ( sin (x + (h / 2)))) / ( - ((1 / 2) * (( cos ((x + (h / 2)) + (x - (h / 2)))) - ( cos ((x + (h / 2)) - (x - (h / 2)))))))) by SIN_COS4: 29

      .= ((( sin (x - (h / 2))) - ( sin (x + (h / 2)))) / (( - (1 / 2)) * (( cos (2 * x)) - ( cos h))))

      .= (((( sin (x - (h / 2))) - ( sin (x + (h / 2)))) / ( - (1 / 2))) / (( cos (2 * x)) - ( cos h))) by XCMPLX_1: 78

      .= (( - 2) * ((( sin (x - (h / 2))) - ( sin (x + (h / 2)))) / (( cos (2 * x)) - ( cos h))));

      hence thesis;

    end;

    theorem :: DIFF_3:65

    (for x holds (f . x) = (1 / ( cos x))) & x0 <> x1 & ( cos x0) <> 0 & ( cos x1) <> 0 implies [!f, x0, x1!] = (((2 * (( cos x1) - ( cos x0))) / (( cos (x0 + x1)) + ( cos (x0 - x1)))) / (x0 - x1))

    proof

      assume that

       A1: for x holds (f . x) = (1 / ( cos x)) and x0 <> x1 and

       A2: ( cos x0) <> 0 & ( cos x1) <> 0 ;

      (f . x0) = (1 / ( cos x0)) & (f . x1) = (1 / ( cos x1)) by A1;

      

      then [!f, x0, x1!] = ((((1 * ( cos x1)) - (1 * ( cos x0))) / (( cos x0) * ( cos x1))) / (x0 - x1)) by A2, XCMPLX_1: 130

      .= (((( cos x1) - ( cos x0)) / ((1 / 2) * (( cos (x0 + x1)) + ( cos (x0 - x1))))) / (x0 - x1)) by SIN_COS4: 32

      .= ((((( cos x1) - ( cos x0)) / (1 / 2)) / (( cos (x0 + x1)) + ( cos (x0 - x1)))) / (x0 - x1)) by XCMPLX_1: 78

      .= ((2 * ((( cos x1) - ( cos x0)) / (( cos (x0 + x1)) + ( cos (x0 - x1))))) / (x0 - x1));

      hence thesis;

    end;

    theorem :: DIFF_3:66

    (for x holds (f . x) = (1 / ( cos x))) & ( cos x) <> 0 & ( cos (x + h)) <> 0 implies (( fD (f,h)) . x) = ((2 * (( cos x) - ( cos (x + h)))) / (( cos ((2 * x) + h)) + ( cos h)))

    proof

      assume that

       A1: for x holds (f . x) = (1 / ( cos x)) and

       A2: ( cos x) <> 0 & ( cos (x + h)) <> 0 ;

      (f . (x + h)) = (1 / ( cos (x + h))) by A1;

      

      then (( fD (f,h)) . x) = ((1 / ( cos (x + h))) - (f . x)) by DIFF_1: 3

      .= ((1 / ( cos (x + h))) - (1 / ( cos x))) by A1

      .= (((1 * ( cos x)) - (1 * ( cos (x + h)))) / (( cos (x + h)) * ( cos x))) by A2, XCMPLX_1: 130

      .= ((( cos x) - ( cos (x + h))) / ((1 / 2) * (( cos ((x + h) + x)) + ( cos ((x + h) - x))))) by SIN_COS4: 32

      .= (((( cos x) - ( cos (x + h))) / (1 / 2)) / (( cos ((2 * x) + h)) + ( cos h))) by XCMPLX_1: 78

      .= (2 * ((( cos x) - ( cos (x + h))) / (( cos ((2 * x) + h)) + ( cos h))));

      hence thesis;

    end;

    theorem :: DIFF_3:67

    (for x holds (f . x) = (1 / ( cos x))) & ( cos x) <> 0 & ( cos (x - h)) <> 0 implies (( bD (f,h)) . x) = ((2 * (( cos (x - h)) - ( cos x))) / (( cos ((2 * x) - h)) + ( cos h)))

    proof

      assume that

       A1: for x holds (f . x) = (1 / ( cos x)) and

       A2: ( cos x) <> 0 & ( cos (x - h)) <> 0 ;

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((1 / ( cos x)) - (f . (x - h))) by A1

      .= ((1 / ( cos x)) - (1 / ( cos (x - h)))) by A1

      .= (((1 * ( cos (x - h))) - (1 * ( cos x))) / (( cos x) * ( cos (x - h)))) by A2, XCMPLX_1: 130

      .= ((( cos (x - h)) - ( cos x)) / ((1 / 2) * (( cos (x + (x - h))) + ( cos (x - (x - h)))))) by SIN_COS4: 32

      .= (((( cos (x - h)) - ( cos x)) / (1 / 2)) / (( cos ((2 * x) - h)) + ( cos h))) by XCMPLX_1: 78

      .= (2 * ((( cos (x - h)) - ( cos x)) / (( cos ((2 * x) - h)) + ( cos h))));

      hence thesis;

    end;

    theorem :: DIFF_3:68

    (for x holds (f . x) = (1 / ( cos x))) & ( cos (x + (h / 2))) <> 0 & ( cos (x - (h / 2))) <> 0 implies (( cD (f,h)) . x) = ((2 * (( cos (x - (h / 2))) - ( cos (x + (h / 2))))) / (( cos (2 * x)) + ( cos h)))

    proof

      assume that

       A1: for x holds (f . x) = (1 / ( cos x)) and

       A2: ( cos (x + (h / 2))) <> 0 & ( cos (x - (h / 2))) <> 0 ;

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= ((1 / ( cos (x + (h / 2)))) - (f . (x - (h / 2)))) by A1

      .= ((1 / ( cos (x + (h / 2)))) - (1 / ( cos (x - (h / 2))))) by A1

      .= (((1 * ( cos (x - (h / 2)))) - (1 * ( cos (x + (h / 2))))) / (( cos (x + (h / 2))) * ( cos (x - (h / 2))))) by A2, XCMPLX_1: 130

      .= ((( cos (x - (h / 2))) - ( cos (x + (h / 2)))) / ((1 / 2) * (( cos ((x + (h / 2)) + (x - (h / 2)))) + ( cos ((x + (h / 2)) - (x - (h / 2))))))) by SIN_COS4: 32

      .= (((( cos (x - (h / 2))) - ( cos (x + (h / 2)))) / (1 / 2)) / (( cos (2 * x)) + ( cos h))) by XCMPLX_1: 78

      .= (2 * ((( cos (x - (h / 2))) - ( cos (x + (h / 2)))) / (( cos (2 * x)) + ( cos h))));

      hence thesis;

    end;

    theorem :: DIFF_3:69

    (for x holds (f . x) = (1 / (( sin x) ^2 ))) & x0 <> x1 & ( sin x0) <> 0 & ( sin x1) <> 0 implies [!f, x0, x1!] = (((((16 * ( cos ((x1 + x0) / 2))) * ( sin ((x1 - x0) / 2))) * ( cos ((x1 - x0) / 2))) * ( sin ((x1 + x0) / 2))) / (((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 ) * (x0 - x1)))

    proof

      assume that

       A1: for x holds (f . x) = (1 / (( sin x) ^2 )) and x0 <> x1 and

       A2: ( sin x0) <> 0 & ( sin x1) <> 0 ;

      (f . x0) = (1 / (( sin x0) ^2 )) & (f . x1) = (1 / (( sin x1) ^2 )) by A1;

      

      then [!f, x0, x1!] = ((((1 * (( sin x1) ^2 )) - (1 * (( sin x0) ^2 ))) / ((( sin x0) ^2 ) * (( sin x1) ^2 ))) / (x0 - x1)) by A2, XCMPLX_1: 130

      .= ((((( sin x1) ^2 ) - (( sin x0) ^2 )) / ((( sin x0) * ( sin x1)) ^2 )) / (x0 - x1))

      .= ((((( sin x1) ^2 ) - (( sin x0) ^2 )) / (( - ((1 / 2) * (( cos (x0 + x1)) - ( cos (x0 - x1))))) ^2 )) / (x0 - x1)) by SIN_COS4: 29

      .= ((((( sin x1) ^2 ) - (( sin x0) ^2 )) / ((1 / 4) * ((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 ))) / (x0 - x1))

      .= (((((( sin x1) ^2 ) - (( sin x0) ^2 )) / (1 / 4)) / ((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 )) / (x0 - x1)) by XCMPLX_1: 78

      .= (((4 * ((( sin x1) - ( sin x0)) * (( sin x1) + ( sin x0)))) / ((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 )) / (x0 - x1))

      .= (((4 * ((2 * (( cos ((x1 + x0) / 2)) * ( sin ((x1 - x0) / 2)))) * (( sin x1) + ( sin x0)))) / ((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 )) / (x0 - x1)) by SIN_COS4: 16

      .= (((4 * ((2 * (( cos ((x1 + x0) / 2)) * ( sin ((x1 - x0) / 2)))) * (2 * (( cos ((x1 - x0) / 2)) * ( sin ((x1 + x0) / 2)))))) / ((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 )) / (x0 - x1)) by SIN_COS4: 15

      .= (((((16 * ( cos ((x1 + x0) / 2))) * ( sin ((x1 - x0) / 2))) * ( cos ((x1 - x0) / 2))) * ( sin ((x1 + x0) / 2))) / (((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 ) * (x0 - x1))) by XCMPLX_1: 78;

      hence thesis;

    end;

    theorem :: DIFF_3:70

    (for x holds (f . x) = (1 / (( sin x) ^2 ))) & ( sin x) <> 0 & ( sin (x + h)) <> 0 implies (( fD (f,h)) . x) = (((((16 * ( cos (((2 * x) + h) / 2))) * ( sin (( - h) / 2))) * ( cos (( - h) / 2))) * ( sin (((2 * x) + h) / 2))) / ((( cos ((2 * x) + h)) - ( cos h)) ^2 ))

    proof

      assume that

       A1: for x holds (f . x) = (1 / (( sin x) ^2 )) and

       A2: ( sin x) <> 0 & ( sin (x + h)) <> 0 ;

      (( fD (f,h)) . x) = ((f . (x + h)) - (f . x)) by DIFF_1: 3

      .= ((1 / (( sin (x + h)) ^2 )) - (f . x)) by A1

      .= ((1 / (( sin (x + h)) ^2 )) - (1 / (( sin x) ^2 ))) by A1

      .= (((1 * (( sin x) ^2 )) - (1 * (( sin (x + h)) ^2 ))) / ((( sin (x + h)) ^2 ) * (( sin x) ^2 ))) by A2, XCMPLX_1: 130

      .= (((( sin x) ^2 ) - (( sin (x + h)) ^2 )) / ((( sin (x + h)) * ( sin x)) ^2 ))

      .= (((( sin x) ^2 ) - (( sin (x + h)) ^2 )) / (( - ((1 / 2) * (( cos ((x + h) + x)) - ( cos ((x + h) - x))))) ^2 )) by SIN_COS4: 29

      .= (((( sin x) ^2 ) - (( sin (x + h)) ^2 )) / ((1 / 4) * ((( cos ((2 * x) + h)) - ( cos h)) ^2 )))

      .= ((((( sin x) ^2 ) - (( sin (x + h)) ^2 )) / (1 / 4)) / ((( cos ((2 * x) + h)) - ( cos h)) ^2 )) by XCMPLX_1: 78

      .= (4 * (((( sin x) - ( sin (x + h))) * (( sin x) + ( sin (x + h)))) / ((( cos ((2 * x) + h)) - ( cos h)) ^2 )))

      .= (4 * (((2 * (( cos ((x + (x + h)) / 2)) * ( sin ((x - (x + h)) / 2)))) * (( sin x) + ( sin (x + h)))) / ((( cos ((2 * x) + h)) - ( cos h)) ^2 ))) by SIN_COS4: 16

      .= (4 * (((2 * (( cos (((2 * x) + h) / 2)) * ( sin (( - h) / 2)))) * (2 * (( cos (( - h) / 2)) * ( sin (((2 * x) + h) / 2))))) / ((( cos ((2 * x) + h)) - ( cos h)) ^2 ))) by SIN_COS4: 15

      .= (((((16 * ( cos (((2 * x) + h) / 2))) * ( sin (( - h) / 2))) * ( cos (( - h) / 2))) * ( sin (((2 * x) + h) / 2))) / ((( cos ((2 * x) + h)) - ( cos h)) ^2 ));

      hence thesis;

    end;

    theorem :: DIFF_3:71

    (for x holds (f . x) = (1 / (( sin x) ^2 ))) & ( sin x) <> 0 & ( sin (x - h)) <> 0 implies (( bD (f,h)) . x) = (((((16 * ( cos (((2 * x) - h) / 2))) * ( sin (( - h) / 2))) * ( cos (( - h) / 2))) * ( sin (((2 * x) - h) / 2))) / ((( cos ((2 * x) - h)) - ( cos h)) ^2 ))

    proof

      assume that

       A1: for x holds (f . x) = (1 / (( sin x) ^2 )) and

       A2: ( sin x) <> 0 & ( sin (x - h)) <> 0 ;

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((1 / (( sin x) ^2 )) - (f . (x - h))) by A1

      .= ((1 / (( sin x) ^2 )) - (1 / (( sin (x - h)) ^2 ))) by A1

      .= (((1 * (( sin (x - h)) ^2 )) - (1 * (( sin x) ^2 ))) / ((( sin x) ^2 ) * (( sin (x - h)) ^2 ))) by A2, XCMPLX_1: 130

      .= (((( sin (x - h)) ^2 ) - (( sin x) ^2 )) / ((( sin x) * ( sin (x - h))) ^2 ))

      .= (((( sin (x - h)) ^2 ) - (( sin x) ^2 )) / (( - ((1 / 2) * (( cos (x + (x - h))) - ( cos (x - (x - h)))))) ^2 )) by SIN_COS4: 29

      .= (((( sin (x - h)) ^2 ) - (( sin x) ^2 )) / ((1 / 4) * ((( cos ((2 * x) - h)) - ( cos h)) ^2 )))

      .= ((((( sin (x - h)) ^2 ) - (( sin x) ^2 )) / (1 / 4)) / ((( cos ((2 * x) - h)) - ( cos h)) ^2 )) by XCMPLX_1: 78

      .= (4 * (((( sin (x - h)) - ( sin x)) * (( sin (x - h)) + ( sin x))) / ((( cos ((2 * x) - h)) - ( cos h)) ^2 )))

      .= (4 * (((2 * (( cos (((x - h) + x) / 2)) * ( sin (((x - h) - x) / 2)))) * (( sin (x - h)) + ( sin x))) / ((( cos ((2 * x) - h)) - ( cos h)) ^2 ))) by SIN_COS4: 16

      .= (4 * (((2 * (( cos (((2 * x) - h) / 2)) * ( sin (( - h) / 2)))) * (2 * (( cos (( - h) / 2)) * ( sin (((2 * x) - h) / 2))))) / ((( cos ((2 * x) - h)) - ( cos h)) ^2 ))) by SIN_COS4: 15

      .= (((((16 * ( cos (((2 * x) - h) / 2))) * ( sin (( - h) / 2))) * ( cos (( - h) / 2))) * ( sin (((2 * x) - h) / 2))) / ((( cos ((2 * x) - h)) - ( cos h)) ^2 ));

      hence thesis;

    end;

    theorem :: DIFF_3:72

    (for x holds (f . x) = (1 / (( sin x) ^2 ))) & ( sin (x + (h / 2))) <> 0 & ( sin (x - (h / 2))) <> 0 implies (( cD (f,h)) . x) = (((((16 * ( cos x)) * ( sin (( - h) / 2))) * ( cos (( - h) / 2))) * ( sin x)) / ((( cos (2 * x)) - ( cos h)) ^2 ))

    proof

      assume that

       A1: for x holds (f . x) = (1 / (( sin x) ^2 )) and

       A2: ( sin (x + (h / 2))) <> 0 & ( sin (x - (h / 2))) <> 0 ;

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= ((1 / (( sin (x + (h / 2))) ^2 )) - (f . (x - (h / 2)))) by A1

      .= ((1 / (( sin (x + (h / 2))) ^2 )) - (1 / (( sin (x - (h / 2))) ^2 ))) by A1

      .= (((1 * (( sin (x - (h / 2))) ^2 )) - (1 * (( sin (x + (h / 2))) ^2 ))) / ((( sin (x + (h / 2))) ^2 ) * (( sin (x - (h / 2))) ^2 ))) by A2, XCMPLX_1: 130

      .= (((( sin (x - (h / 2))) ^2 ) - (( sin (x + (h / 2))) ^2 )) / ((( sin (x + (h / 2))) * ( sin (x - (h / 2)))) ^2 ))

      .= (((( sin (x - (h / 2))) ^2 ) - (( sin (x + (h / 2))) ^2 )) / (( - ((1 / 2) * (( cos ((x + (h / 2)) + (x - (h / 2)))) - ( cos ((x + (h / 2)) - (x - (h / 2))))))) ^2 )) by SIN_COS4: 29

      .= (((( sin (x - (h / 2))) ^2 ) - (( sin (x + (h / 2))) ^2 )) / ((1 / 4) * ((( cos (2 * x)) - ( cos h)) ^2 )))

      .= ((((( sin (x - (h / 2))) ^2 ) - (( sin (x + (h / 2))) ^2 )) / (1 / 4)) / ((( cos (2 * x)) - ( cos h)) ^2 )) by XCMPLX_1: 78

      .= (4 * (((( sin (x - (h / 2))) - ( sin (x + (h / 2)))) * (( sin (x - (h / 2))) + ( sin (x + (h / 2))))) / ((( cos (2 * x)) - ( cos h)) ^2 )))

      .= (4 * (((2 * (( cos (((x - (h / 2)) + (x + (h / 2))) / 2)) * ( sin (((x - (h / 2)) - (x + (h / 2))) / 2)))) * (( sin (x - (h / 2))) + ( sin (x + (h / 2))))) / ((( cos (2 * x)) - ( cos h)) ^2 ))) by SIN_COS4: 16

      .= (4 * (((2 * (( cos ((2 * x) / 2)) * ( sin (( - h) / 2)))) * (2 * (( cos (( - h) / 2)) * ( sin ((2 * x) / 2))))) / ((( cos (2 * x)) - ( cos h)) ^2 ))) by SIN_COS4: 15

      .= (((((16 * ( cos x)) * ( sin (( - h) / 2))) * ( cos (( - h) / 2))) * ( sin x)) / ((( cos (2 * x)) - ( cos h)) ^2 ));

      hence thesis;

    end;

    theorem :: DIFF_3:73

    (for x holds (f . x) = (1 / (( cos x) ^2 ))) & x0 <> x1 & ( cos x0) <> 0 & ( cos x1) <> 0 implies [!f, x0, x1!] = ((((((( - 16) * ( sin ((x1 + x0) / 2))) * ( sin ((x1 - x0) / 2))) * ( cos ((x1 + x0) / 2))) * ( cos ((x1 - x0) / 2))) / ((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 )) / (x0 - x1))

    proof

      assume that

       A1: for x holds (f . x) = (1 / (( cos x) ^2 )) and x0 <> x1 and

       A2: ( cos x0) <> 0 & ( cos x1) <> 0 ;

      (f . x0) = (1 / (( cos x0) ^2 )) & (f . x1) = (1 / (( cos x1) ^2 )) by A1;

      

      then [!f, x0, x1!] = ((((1 * (( cos x1) ^2 )) - (1 * (( cos x0) ^2 ))) / ((( cos x0) ^2 ) * (( cos x1) ^2 ))) / (x0 - x1)) by A2, XCMPLX_1: 130

      .= ((((( cos x1) ^2 ) - (( cos x0) ^2 )) / ((( cos x0) * ( cos x1)) ^2 )) / (x0 - x1))

      .= ((((( cos x1) ^2 ) - (( cos x0) ^2 )) / (((1 / 2) * (( cos (x0 + x1)) + ( cos (x0 - x1)))) ^2 )) / (x0 - x1)) by SIN_COS4: 32

      .= ((((( cos x1) ^2 ) - (( cos x0) ^2 )) / ((1 / 4) * ((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 ))) / (x0 - x1))

      .= (((((( cos x1) ^2 ) - (( cos x0) ^2 )) / (1 / 4)) / ((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 )) / (x0 - x1)) by XCMPLX_1: 78

      .= (((4 * ((( cos x1) - ( cos x0)) * (( cos x1) + ( cos x0)))) / ((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 )) / (x0 - x1))

      .= (((4 * (( - (2 * (( sin ((x1 + x0) / 2)) * ( sin ((x1 - x0) / 2))))) * (( cos x1) + ( cos x0)))) / ((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 )) / (x0 - x1)) by SIN_COS4: 18

      .= (((4 * (( - (2 * (( sin ((x1 + x0) / 2)) * ( sin ((x1 - x0) / 2))))) * (2 * (( cos ((x1 + x0) / 2)) * ( cos ((x1 - x0) / 2)))))) / ((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 )) / (x0 - x1)) by SIN_COS4: 17

      .= ((((((( - 16) * ( sin ((x1 + x0) / 2))) * ( sin ((x1 - x0) / 2))) * ( cos ((x1 + x0) / 2))) * ( cos ((x1 - x0) / 2))) / ((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 )) / (x0 - x1));

      hence thesis;

    end;

    theorem :: DIFF_3:74

    (for x holds (f . x) = (1 / (( cos x) ^2 ))) & ( cos x) <> 0 & ( cos (x + h)) <> 0 implies (( fD (f,h)) . x) = (((((( - 16) * ( sin (((2 * x) + h) / 2))) * ( sin (( - h) / 2))) * ( cos (((2 * x) + h) / 2))) * ( cos (( - h) / 2))) / ((( cos ((2 * x) + h)) + ( cos h)) ^2 ))

    proof

      assume that

       A1: for x holds (f . x) = (1 / (( cos x) ^2 )) and

       A2: ( cos x) <> 0 & ( cos (x + h)) <> 0 ;

      (( fD (f,h)) . x) = ((f . (x + h)) - (f . x)) by DIFF_1: 3

      .= ((1 / (( cos (x + h)) ^2 )) - (f . x)) by A1

      .= ((1 / (( cos (x + h)) ^2 )) - (1 / (( cos x) ^2 ))) by A1

      .= (((1 * (( cos x) ^2 )) - (1 * (( cos (x + h)) ^2 ))) / ((( cos (x + h)) ^2 ) * (( cos x) ^2 ))) by A2, XCMPLX_1: 130

      .= (((( cos x) ^2 ) - (( cos (x + h)) ^2 )) / ((( cos (x + h)) * ( cos x)) ^2 ))

      .= (((( cos x) ^2 ) - (( cos (x + h)) ^2 )) / (((1 / 2) * (( cos ((x + h) + x)) + ( cos ((x + h) - x)))) ^2 )) by SIN_COS4: 32

      .= (((( cos x) ^2 ) - (( cos (x + h)) ^2 )) / ((1 / 4) * ((( cos ((2 * x) + h)) + ( cos h)) ^2 )))

      .= ((((( cos x) ^2 ) - (( cos (x + h)) ^2 )) / (1 / 4)) / ((( cos ((2 * x) + h)) + ( cos h)) ^2 )) by XCMPLX_1: 78

      .= (4 * (((( cos x) - ( cos (x + h))) * (( cos x) + ( cos (x + h)))) / ((( cos ((2 * x) + h)) + ( cos h)) ^2 )))

      .= (4 * ((( - (2 * (( sin ((x + (x + h)) / 2)) * ( sin ((x - (x + h)) / 2))))) * (( cos x) + ( cos (x + h)))) / ((( cos ((2 * x) + h)) + ( cos h)) ^2 ))) by SIN_COS4: 18

      .= (4 * ((( - (2 * (( sin (((2 * x) + h) / 2)) * ( sin (( - h) / 2))))) * (2 * (( cos (((2 * x) + h) / 2)) * ( cos (( - h) / 2))))) / ((( cos ((2 * x) + h)) + ( cos h)) ^2 ))) by SIN_COS4: 17

      .= (((((( - 16) * ( sin (((2 * x) + h) / 2))) * ( sin (( - h) / 2))) * ( cos (((2 * x) + h) / 2))) * ( cos (( - h) / 2))) / ((( cos ((2 * x) + h)) + ( cos h)) ^2 ));

      hence thesis;

    end;

    theorem :: DIFF_3:75

    (for x holds (f . x) = (1 / (( cos x) ^2 ))) & ( cos x) <> 0 & ( cos (x - h)) <> 0 implies (( bD (f,h)) . x) = (((((( - 16) * ( sin (((2 * x) - h) / 2))) * ( sin (( - h) / 2))) * ( cos (((2 * x) - h) / 2))) * ( cos (( - h) / 2))) / ((( cos ((2 * x) - h)) + ( cos h)) ^2 ))

    proof

      assume that

       A1: for x holds (f . x) = (1 / (( cos x) ^2 )) and

       A2: ( cos x) <> 0 & ( cos (x - h)) <> 0 ;

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((1 / (( cos x) ^2 )) - (f . (x - h))) by A1

      .= ((1 / (( cos x) ^2 )) - (1 / (( cos (x - h)) ^2 ))) by A1

      .= (((1 * (( cos (x - h)) ^2 )) - (1 * (( cos x) ^2 ))) / ((( cos x) ^2 ) * (( cos (x - h)) ^2 ))) by A2, XCMPLX_1: 130

      .= (((( cos (x - h)) ^2 ) - (( cos x) ^2 )) / ((( cos x) * ( cos (x - h))) ^2 ))

      .= (((( cos (x - h)) ^2 ) - (( cos x) ^2 )) / (((1 / 2) * (( cos (x + (x - h))) + ( cos (x - (x - h))))) ^2 )) by SIN_COS4: 32

      .= (((( cos (x - h)) ^2 ) - (( cos x) ^2 )) / ((1 / 4) * ((( cos ((2 * x) - h)) + ( cos h)) ^2 )))

      .= ((((( cos (x - h)) ^2 ) - (( cos x) ^2 )) / (1 / 4)) / ((( cos ((2 * x) - h)) + ( cos h)) ^2 )) by XCMPLX_1: 78

      .= (4 * (((( cos (x - h)) - ( cos x)) * (( cos (x - h)) + ( cos x))) / ((( cos ((2 * x) - h)) + ( cos h)) ^2 )))

      .= (4 * ((( - (2 * (( sin (((x - h) + x) / 2)) * ( sin (((x - h) - x) / 2))))) * (( cos (x - h)) + ( cos x))) / ((( cos ((2 * x) - h)) + ( cos h)) ^2 ))) by SIN_COS4: 18

      .= (4 * ((( - (2 * (( sin (((2 * x) - h) / 2)) * ( sin (( - h) / 2))))) * (2 * (( cos (((2 * x) - h) / 2)) * ( cos (( - h) / 2))))) / ((( cos ((2 * x) - h)) + ( cos h)) ^2 ))) by SIN_COS4: 17

      .= (((((( - 16) * ( sin (((2 * x) - h) / 2))) * ( sin (( - h) / 2))) * ( cos (((2 * x) - h) / 2))) * ( cos (( - h) / 2))) / ((( cos ((2 * x) - h)) + ( cos h)) ^2 ));

      hence thesis;

    end;

    theorem :: DIFF_3:76

    (for x holds (f . x) = (1 / (( cos x) ^2 ))) & ( cos (x + (h / 2))) <> 0 & ( cos (x - (h / 2))) <> 0 implies (( cD (f,h)) . x) = (((((( - 16) * ( sin x)) * ( sin (( - h) / 2))) * ( cos x)) * ( cos (( - h) / 2))) / ((( cos (2 * x)) + ( cos h)) ^2 ))

    proof

      assume that

       A1: for x holds (f . x) = (1 / (( cos x) ^2 )) and

       A2: ( cos (x + (h / 2))) <> 0 & ( cos (x - (h / 2))) <> 0 ;

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= ((1 / (( cos (x + (h / 2))) ^2 )) - (f . (x - (h / 2)))) by A1

      .= ((1 / (( cos (x + (h / 2))) ^2 )) - (1 / (( cos (x - (h / 2))) ^2 ))) by A1

      .= (((1 * (( cos (x - (h / 2))) ^2 )) - (1 * (( cos (x + (h / 2))) ^2 ))) / ((( cos (x + (h / 2))) ^2 ) * (( cos (x - (h / 2))) ^2 ))) by A2, XCMPLX_1: 130

      .= (((( cos (x - (h / 2))) ^2 ) - (( cos (x + (h / 2))) ^2 )) / ((( cos (x + (h / 2))) * ( cos (x - (h / 2)))) ^2 ))

      .= (((( cos (x - (h / 2))) ^2 ) - (( cos (x + (h / 2))) ^2 )) / (((1 / 2) * (( cos ((x + (h / 2)) + (x - (h / 2)))) + ( cos ((x + (h / 2)) - (x - (h / 2)))))) ^2 )) by SIN_COS4: 32

      .= (((( cos (x - (h / 2))) ^2 ) - (( cos (x + (h / 2))) ^2 )) / ((1 / 4) * ((( cos (2 * x)) + ( cos h)) ^2 )))

      .= ((((( cos (x - (h / 2))) ^2 ) - (( cos (x + (h / 2))) ^2 )) / (1 / 4)) / ((( cos (2 * x)) + ( cos h)) ^2 )) by XCMPLX_1: 78

      .= (4 * (((( cos (x - (h / 2))) - ( cos (x + (h / 2)))) * (( cos (x - (h / 2))) + ( cos (x + (h / 2))))) / ((( cos (2 * x)) + ( cos h)) ^2 )))

      .= (4 * ((( - (2 * (( sin (((x - (h / 2)) + (x + (h / 2))) / 2)) * ( sin (((x - (h / 2)) - (x + (h / 2))) / 2))))) * (( cos (x - (h / 2))) + ( cos (x + (h / 2))))) / ((( cos (2 * x)) + ( cos h)) ^2 ))) by SIN_COS4: 18

      .= (4 * ((( - (2 * (( sin ((2 * x) / 2)) * ( sin (( - h) / 2))))) * (2 * (( cos ((2 * x) / 2)) * ( cos (( - h) / 2))))) / ((( cos (2 * x)) + ( cos h)) ^2 ))) by SIN_COS4: 17

      .= (((((( - 16) * ( sin x)) * ( sin (( - h) / 2))) * ( cos x)) * ( cos (( - h) / 2))) / ((( cos (2 * x)) + ( cos h)) ^2 ));

      hence thesis;

    end;

    theorem :: DIFF_3:77

    x0 in ( dom tan ) & x1 in ( dom tan ) implies [!( tan (#) sin ), x0, x1!] = (((((1 / ( cos x0)) - ( cos x0)) - (1 / ( cos x1))) + ( cos x1)) / (x0 - x1))

    proof

      assume

       A1: x0 in ( dom tan ) & x1 in ( dom tan );

       [!( tan (#) sin ), x0, x1!] = (((( tan . x0) * ( sin . x0)) - (( tan (#) sin ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= (((( tan . x0) * ( sin . x0)) - (( tan . x1) * ( sin . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( sin . x0) * (( cos . x0) " )) * ( sin . x0)) - (( tan . x1) * ( sin . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= ((((( sin x0) / ( cos x0)) * ( sin x0)) - ((( sin x1) / ( cos x1)) * ( sin x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((( sin x0) / (( cos x0) / ( sin x0))) - ((( sin x1) / ( cos x1)) * ( sin x1))) / (x0 - x1)) by XCMPLX_1: 82

      .= (((( sin x0) / (( cos x0) / ( sin x0))) - (( sin x1) / (( cos x1) / ( sin x1)))) / (x0 - x1)) by XCMPLX_1: 82

      .= ((((( sin x0) * ( sin x0)) / ( cos x0)) - (( sin x1) / (( cos x1) / ( sin x1)))) / (x0 - x1)) by XCMPLX_1: 77

      .= ((((( sin x0) * ( sin x0)) / ( cos x0)) - ((( sin x1) * ( sin x1)) / ( cos x1))) / (x0 - x1)) by XCMPLX_1: 77

      .= ((((1 - (( cos x0) * ( cos x0))) / ( cos x0)) - ((( sin x1) * ( sin x1)) / ( cos x1))) / (x0 - x1)) by SIN_COS4: 4

      .= ((((1 / ( cos x0)) - ((( cos x0) * ( cos x0)) / ( cos x0))) - ((1 - (( cos x1) * ( cos x1))) / ( cos x1))) / (x0 - x1)) by SIN_COS4: 4

      .= ((((1 / ( cos x0)) - ( cos x0)) - ((1 / ( cos x1)) - ((( cos x1) * ( cos x1)) / ( cos x1)))) / (x0 - x1)) by A1, FDIFF_8: 1, XCMPLX_1: 89

      .= ((((1 / ( cos x0)) - ( cos x0)) - ((1 / ( cos x1)) - ( cos x1))) / (x0 - x1)) by A1, FDIFF_8: 1, XCMPLX_1: 89

      .= (((((1 / ( cos x0)) - ( cos x0)) - (1 / ( cos x1))) + ( cos x1)) / (x0 - x1));

      hence thesis;

    end;

    theorem :: DIFF_3:78

    (for x holds (f . x) = (( tan (#) sin ) . x)) & x in ( dom tan ) & (x + h) in ( dom tan ) implies (( fD (f,h)) . x) = ((((1 / ( cos (x + h))) - ( cos (x + h))) - (1 / ( cos x))) + ( cos x))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) sin ) . x) and

       A2: x in ( dom tan ) & (x + h) in ( dom tan );

      (( fD (f,h)) . x) = ((f . (x + h)) - (f . x)) by DIFF_1: 3

      .= ((( tan (#) sin ) . (x + h)) - (f . x)) by A1

      .= ((( tan (#) sin ) . (x + h)) - (( tan (#) sin ) . x)) by A1

      .= ((( tan . (x + h)) * ( sin . (x + h))) - (( tan (#) sin ) . x)) by VALUED_1: 5

      .= ((( tan . (x + h)) * ( sin . (x + h))) - (( tan . x) * ( sin . x))) by VALUED_1: 5

      .= (((( sin . (x + h)) * (( cos . (x + h)) " )) * ( sin . (x + h))) - (( tan . x) * ( sin . x))) by A2, RFUNCT_1:def 1

      .= (((( sin (x + h)) / ( cos (x + h))) * ( sin (x + h))) - ((( sin x) / ( cos x)) * ( sin x))) by A2, RFUNCT_1:def 1

      .= ((( sin (x + h)) / (( cos (x + h)) / ( sin (x + h)))) - ((( sin x) / ( cos x)) * ( sin x))) by XCMPLX_1: 82

      .= ((( sin (x + h)) / (( cos (x + h)) / ( sin (x + h)))) - (( sin x) / (( cos x) / ( sin x)))) by XCMPLX_1: 82

      .= (((( sin (x + h)) * ( sin (x + h))) / ( cos (x + h))) - (( sin x) / (( cos x) / ( sin x)))) by XCMPLX_1: 77

      .= (((( sin (x + h)) * ( sin (x + h))) / ( cos (x + h))) - ((( sin x) * ( sin x)) / ( cos x))) by XCMPLX_1: 77

      .= (((1 - (( cos (x + h)) * ( cos (x + h)))) / ( cos (x + h))) - ((( sin x) * ( sin x)) / ( cos x))) by SIN_COS4: 4

      .= (((1 / ( cos (x + h))) - ((( cos (x + h)) * ( cos (x + h))) / ( cos (x + h)))) - ((1 - (( cos x) * ( cos x))) / ( cos x))) by SIN_COS4: 4

      .= (((1 / ( cos (x + h))) - ( cos (x + h))) - ((1 / ( cos x)) - ((( cos x) * ( cos x)) / ( cos x)))) by A2, FDIFF_8: 1, XCMPLX_1: 89

      .= (((1 / ( cos (x + h))) - ( cos (x + h))) - ((1 / ( cos x)) - ( cos x))) by A2, FDIFF_8: 1, XCMPLX_1: 89

      .= ((((1 / ( cos (x + h))) - ( cos (x + h))) - (1 / ( cos x))) + ( cos x));

      hence thesis;

    end;

    theorem :: DIFF_3:79

    (for x holds (f . x) = (( tan (#) sin ) . x)) & x in ( dom tan ) & (x - h) in ( dom tan ) implies (( bD (f,h)) . x) = ((((1 / ( cos x)) - ( cos x)) - (1 / ( cos (x - h)))) + ( cos (x - h)))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) sin ) . x) and

       A2: x in ( dom tan ) & (x - h) in ( dom tan );

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((( tan (#) sin ) . x) - (f . (x - h))) by A1

      .= ((( tan (#) sin ) . x) - (( tan (#) sin ) . (x - h))) by A1

      .= ((( tan . x) * ( sin . x)) - (( tan (#) sin ) . (x - h))) by VALUED_1: 5

      .= ((( tan . x) * ( sin . x)) - (( tan . (x - h)) * ( sin . (x - h)))) by VALUED_1: 5

      .= (((( sin . x) * (( cos . x) " )) * ( sin . x)) - (( tan . (x - h)) * ( sin . (x - h)))) by A2, RFUNCT_1:def 1

      .= (((( sin x) / ( cos x)) * ( sin x)) - ((( sin (x - h)) / ( cos (x - h))) * ( sin (x - h)))) by A2, RFUNCT_1:def 1

      .= ((( sin x) / (( cos x) / ( sin x))) - ((( sin (x - h)) / ( cos (x - h))) * ( sin (x - h)))) by XCMPLX_1: 82

      .= ((( sin x) / (( cos x) / ( sin x))) - (( sin (x - h)) / (( cos (x - h)) / ( sin (x - h))))) by XCMPLX_1: 82

      .= (((( sin x) * ( sin x)) / ( cos x)) - (( sin (x - h)) / (( cos (x - h)) / ( sin (x - h))))) by XCMPLX_1: 77

      .= (((( sin x) * ( sin x)) / ( cos x)) - ((( sin (x - h)) * ( sin (x - h))) / ( cos (x - h)))) by XCMPLX_1: 77

      .= (((1 - (( cos x) * ( cos x))) / ( cos x)) - ((( sin (x - h)) * ( sin (x - h))) / ( cos (x - h)))) by SIN_COS4: 4

      .= (((1 / ( cos x)) - ((( cos x) * ( cos x)) / ( cos x))) - ((1 - (( cos (x - h)) * ( cos (x - h)))) / ( cos (x - h)))) by SIN_COS4: 4

      .= (((1 / ( cos x)) - ( cos x)) - ((1 / ( cos (x - h))) - ((( cos (x - h)) * ( cos (x - h))) / ( cos (x - h))))) by A2, FDIFF_8: 1, XCMPLX_1: 89

      .= (((1 / ( cos x)) - ( cos x)) - ((1 / ( cos (x - h))) - ( cos (x - h)))) by A2, FDIFF_8: 1, XCMPLX_1: 89

      .= ((((1 / ( cos x)) - ( cos x)) - (1 / ( cos (x - h)))) + ( cos (x - h)));

      hence thesis;

    end;

    theorem :: DIFF_3:80

    (for x holds (f . x) = (( tan (#) sin ) . x)) & (x + (h / 2)) in ( dom tan ) & (x - (h / 2)) in ( dom tan ) implies (( cD (f,h)) . x) = ((((1 / ( cos (x + (h / 2)))) - ( cos (x + (h / 2)))) - (1 / ( cos (x - (h / 2))))) + ( cos (x - (h / 2))))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) sin ) . x) and

       A2: (x + (h / 2)) in ( dom tan ) & (x - (h / 2)) in ( dom tan );

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= ((( tan (#) sin ) . (x + (h / 2))) - (f . (x - (h / 2)))) by A1

      .= ((( tan (#) sin ) . (x + (h / 2))) - (( tan (#) sin ) . (x - (h / 2)))) by A1

      .= ((( tan . (x + (h / 2))) * ( sin . (x + (h / 2)))) - (( tan (#) sin ) . (x - (h / 2)))) by VALUED_1: 5

      .= ((( tan . (x + (h / 2))) * ( sin . (x + (h / 2)))) - (( tan . (x - (h / 2))) * ( sin . (x - (h / 2))))) by VALUED_1: 5

      .= (((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * ( sin . (x + (h / 2)))) - (( tan . (x - (h / 2))) * ( sin . (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= (((( sin (x + (h / 2))) / ( cos (x + (h / 2)))) * ( sin (x + (h / 2)))) - ((( sin (x - (h / 2))) / ( cos (x - (h / 2)))) * ( sin (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= ((( sin (x + (h / 2))) / (( cos (x + (h / 2))) / ( sin (x + (h / 2))))) - ((( sin (x - (h / 2))) / ( cos (x - (h / 2)))) * ( sin (x - (h / 2))))) by XCMPLX_1: 82

      .= ((( sin (x + (h / 2))) / (( cos (x + (h / 2))) / ( sin (x + (h / 2))))) - (( sin (x - (h / 2))) / (( cos (x - (h / 2))) / ( sin (x - (h / 2)))))) by XCMPLX_1: 82

      .= (((( sin (x + (h / 2))) * ( sin (x + (h / 2)))) / ( cos (x + (h / 2)))) - (( sin (x - (h / 2))) / (( cos (x - (h / 2))) / ( sin (x - (h / 2)))))) by XCMPLX_1: 77

      .= (((( sin (x + (h / 2))) * ( sin (x + (h / 2)))) / ( cos (x + (h / 2)))) - ((( sin (x - (h / 2))) * ( sin (x - (h / 2)))) / ( cos (x - (h / 2))))) by XCMPLX_1: 77

      .= (((1 - (( cos (x + (h / 2))) * ( cos (x + (h / 2))))) / ( cos (x + (h / 2)))) - ((( sin (x - (h / 2))) * ( sin (x - (h / 2)))) / ( cos (x - (h / 2))))) by SIN_COS4: 4

      .= (((1 / ( cos (x + (h / 2)))) - ((( cos (x + (h / 2))) * ( cos (x + (h / 2)))) / ( cos (x + (h / 2))))) - ((1 - (( cos (x - (h / 2))) * ( cos (x - (h / 2))))) / ( cos (x - (h / 2))))) by SIN_COS4: 4

      .= (((1 / ( cos (x + (h / 2)))) - ( cos (x + (h / 2)))) - ((1 / ( cos (x - (h / 2)))) - ((( cos (x - (h / 2))) * ( cos (x - (h / 2)))) / ( cos (x - (h / 2)))))) by A2, FDIFF_8: 1, XCMPLX_1: 89

      .= (((1 / ( cos (x + (h / 2)))) - ( cos (x + (h / 2)))) - ((1 / ( cos (x - (h / 2)))) - ( cos (x - (h / 2))))) by A2, FDIFF_8: 1, XCMPLX_1: 89

      .= ((((1 / ( cos (x + (h / 2)))) - ( cos (x + (h / 2)))) - (1 / ( cos (x - (h / 2))))) + ( cos (x - (h / 2))));

      hence thesis;

    end;

    theorem :: DIFF_3:81

    (for x holds (f . x) = (( tan (#) cos ) . x)) & x0 in ( dom tan ) & x1 in ( dom tan ) implies [!f, x0, x1!] = ((( sin x0) - ( sin x1)) / (x0 - x1))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) cos ) . x) and

       A2: x0 in ( dom tan ) & x1 in ( dom tan );

      

       A3: (f . x0) = (( tan (#) cos ) . x0) by A1;

      (f . x1) = (( tan (#) cos ) . x1) by A1;

      

      then [!f, x0, x1!] = (((( tan . x0) * ( cos . x0)) - (( tan (#) cos ) . x1)) / (x0 - x1)) by A3, VALUED_1: 5

      .= (((( tan . x0) * ( cos . x0)) - (( tan . x1) * ( cos . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( sin . x0) * (( cos . x0) " )) * ( cos . x0)) - (( tan . x1) * ( cos . x1))) / (x0 - x1)) by A2, RFUNCT_1:def 1

      .= ((((( sin x0) / ( cos x0)) * ( cos x0)) - ((( sin x1) / ( cos x1)) * ( cos x1))) / (x0 - x1)) by A2, RFUNCT_1:def 1

      .= (((( sin x0) / (( cos x0) / ( cos x0))) - ((( sin x1) / ( cos x1)) * ( cos x1))) / (x0 - x1)) by XCMPLX_1: 82

      .= (((( sin x0) / (( cos x0) * (1 / ( cos x0)))) - (( sin x1) / (( cos x1) / ( cos x1)))) / (x0 - x1)) by XCMPLX_1: 82

      .= (((( sin x0) / 1) - (( sin x1) / (( cos x1) * (1 / ( cos x1))))) / (x0 - x1)) by A2, FDIFF_8: 1, XCMPLX_1: 106

      .= (((( sin x0) / 1) - (( sin x1) / 1)) / (x0 - x1)) by A2, FDIFF_8: 1, XCMPLX_1: 106

      .= ((( sin x0) - ( sin x1)) / (x0 - x1));

      hence thesis;

    end;

    theorem :: DIFF_3:82

    (for x holds (f . x) = (( tan (#) cos ) . x)) & x in ( dom tan ) & (x + h) in ( dom tan ) implies (( fD (f,h)) . x) = (( sin (x + h)) - ( sin x))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) cos ) . x) and

       A2: x in ( dom tan ) & (x + h) in ( dom tan );

      (( fD (f,h)) . x) = ((f . (x + h)) - (f . x)) by DIFF_1: 3

      .= ((( tan (#) cos ) . (x + h)) - (f . x)) by A1

      .= ((( tan (#) cos ) . (x + h)) - (( tan (#) cos ) . x)) by A1

      .= ((( tan . (x + h)) * ( cos . (x + h))) - (( tan (#) cos ) . x)) by VALUED_1: 5

      .= ((( tan . (x + h)) * ( cos . (x + h))) - (( tan . x) * ( cos . x))) by VALUED_1: 5

      .= (((( sin . (x + h)) * (( cos . (x + h)) " )) * ( cos . (x + h))) - (( tan . x) * ( cos . x))) by A2, RFUNCT_1:def 1

      .= (((( sin (x + h)) / ( cos (x + h))) * ( cos (x + h))) - ((( sin x) / ( cos x)) * ( cos x))) by A2, RFUNCT_1:def 1

      .= ((( sin (x + h)) / (( cos (x + h)) / ( cos (x + h)))) - ((( sin x) / ( cos x)) * ( cos x))) by XCMPLX_1: 82

      .= ((( sin (x + h)) / (( cos (x + h)) * (1 / ( cos (x + h))))) - (( sin x) / (( cos x) / ( cos x)))) by XCMPLX_1: 82

      .= ((( sin (x + h)) / 1) - (( sin x) / (( cos x) * (1 / ( cos x))))) by A2, FDIFF_8: 1, XCMPLX_1: 106

      .= ((( sin (x + h)) / 1) - (( sin x) / 1)) by A2, FDIFF_8: 1, XCMPLX_1: 106

      .= (( sin (x + h)) - ( sin x));

      hence thesis;

    end;

    theorem :: DIFF_3:83

    (for x holds (f . x) = (( tan (#) cos ) . x)) & x in ( dom tan ) & (x - h) in ( dom tan ) implies (( bD (f,h)) . x) = (( sin x) - ( sin (x - h)))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) cos ) . x) and

       A2: x in ( dom tan ) & (x - h) in ( dom tan );

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((( tan (#) cos ) . x) - (f . (x - h))) by A1

      .= ((( tan (#) cos ) . x) - (( tan (#) cos ) . (x - h))) by A1

      .= ((( tan . x) * ( cos . x)) - (( tan (#) cos ) . (x - h))) by VALUED_1: 5

      .= ((( tan . x) * ( cos . x)) - (( tan . (x - h)) * ( cos . (x - h)))) by VALUED_1: 5

      .= (((( sin . x) * (( cos . x) " )) * ( cos . x)) - (( tan . (x - h)) * ( cos . (x - h)))) by A2, RFUNCT_1:def 1

      .= (((( sin x) / ( cos x)) * ( cos x)) - ((( sin (x - h)) / ( cos (x - h))) * ( cos (x - h)))) by A2, RFUNCT_1:def 1

      .= ((( sin x) / (( cos x) / ( cos x))) - ((( sin (x - h)) / ( cos (x - h))) * ( cos (x - h)))) by XCMPLX_1: 82

      .= ((( sin x) / (( cos x) * (1 / ( cos x)))) - (( sin (x - h)) / (( cos (x - h)) / ( cos (x - h))))) by XCMPLX_1: 82

      .= ((( sin x) / 1) - (( sin (x - h)) / (( cos (x - h)) * (1 / ( cos (x - h)))))) by A2, FDIFF_8: 1, XCMPLX_1: 106

      .= ((( sin x) / 1) - (( sin (x - h)) / 1)) by A2, FDIFF_8: 1, XCMPLX_1: 106

      .= (( sin x) - ( sin (x - h)));

      hence thesis;

    end;

    theorem :: DIFF_3:84

    (for x holds (f . x) = (( tan (#) cos ) . x)) & (x + (h / 2)) in ( dom tan ) & (x - (h / 2)) in ( dom tan ) implies (( cD (f,h)) . x) = (( sin (x + (h / 2))) - ( sin (x - (h / 2))))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) cos ) . x) and

       A2: (x + (h / 2)) in ( dom tan ) & (x - (h / 2)) in ( dom tan );

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= ((( tan (#) cos ) . (x + (h / 2))) - (f . (x - (h / 2)))) by A1

      .= ((( tan (#) cos ) . (x + (h / 2))) - (( tan (#) cos ) . (x - (h / 2)))) by A1

      .= ((( tan . (x + (h / 2))) * ( cos . (x + (h / 2)))) - (( tan (#) cos ) . (x - (h / 2)))) by VALUED_1: 5

      .= ((( tan . (x + (h / 2))) * ( cos . (x + (h / 2)))) - (( tan . (x - (h / 2))) * ( cos . (x - (h / 2))))) by VALUED_1: 5

      .= (((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * ( cos . (x + (h / 2)))) - (( tan . (x - (h / 2))) * ( cos . (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= (((( sin (x + (h / 2))) / ( cos (x + (h / 2)))) * ( cos (x + (h / 2)))) - ((( sin (x - (h / 2))) / ( cos (x - (h / 2)))) * ( cos (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= ((( sin (x + (h / 2))) / (( cos (x + (h / 2))) / ( cos (x + (h / 2))))) - ((( sin (x - (h / 2))) / ( cos (x - (h / 2)))) * ( cos (x - (h / 2))))) by XCMPLX_1: 82

      .= ((( sin (x + (h / 2))) / (( cos (x + (h / 2))) * (1 / ( cos (x + (h / 2)))))) - (( sin (x - (h / 2))) / (( cos (x - (h / 2))) / ( cos (x - (h / 2)))))) by XCMPLX_1: 82

      .= ((( sin (x + (h / 2))) / 1) - (( sin (x - (h / 2))) / (( cos (x - (h / 2))) * (1 / ( cos (x - (h / 2))))))) by A2, FDIFF_8: 1, XCMPLX_1: 106

      .= ((( sin (x + (h / 2))) / 1) - (( sin (x - (h / 2))) / 1)) by A2, FDIFF_8: 1, XCMPLX_1: 106

      .= (( sin (x + (h / 2))) - ( sin (x - (h / 2))));

      hence thesis;

    end;

    theorem :: DIFF_3:85

    (for x holds (f . x) = (( cot (#) cos ) . x)) & x0 in ( dom cot ) & x1 in ( dom cot ) implies [!f, x0, x1!] = (((((1 / ( sin x0)) - ( sin x0)) - (1 / ( sin x1))) + ( sin x1)) / (x0 - x1))

    proof

      assume that

       A1: for x holds (f . x) = (( cot (#) cos ) . x) and

       A2: x0 in ( dom cot ) & x1 in ( dom cot );

      

       A3: (f . x0) = (( cot (#) cos ) . x0) by A1;

      (f . x1) = (( cot (#) cos ) . x1) by A1;

      

      then [!f, x0, x1!] = (((( cot . x0) * ( cos . x0)) - (( cot (#) cos ) . x1)) / (x0 - x1)) by A3, VALUED_1: 5

      .= (((( cot . x0) * ( cos . x0)) - (( cot . x1) * ( cos . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cos . x0) * (( sin . x0) " )) * ( cos . x0)) - (( cot . x1) * ( cos . x1))) / (x0 - x1)) by A2, RFUNCT_1:def 1

      .= ((((( cos x0) / ( sin x0)) * ( cos x0)) - ((( cos x1) / ( sin x1)) * ( cos x1))) / (x0 - x1)) by A2, RFUNCT_1:def 1

      .= (((( cos x0) / (( sin x0) / ( cos x0))) - ((( cos x1) / ( sin x1)) * ( cos x1))) / (x0 - x1)) by XCMPLX_1: 82

      .= (((( cos x0) / (( sin x0) / ( cos x0))) - (( cos x1) / (( sin x1) / ( cos x1)))) / (x0 - x1)) by XCMPLX_1: 82

      .= ((((( cos x0) * ( cos x0)) / ( sin x0)) - (( cos x1) / (( sin x1) / ( cos x1)))) / (x0 - x1)) by XCMPLX_1: 77

      .= ((((( cos x0) * ( cos x0)) / ( sin x0)) - ((( cos x1) * ( cos x1)) / ( sin x1))) / (x0 - x1)) by XCMPLX_1: 77

      .= ((((1 - (( sin x0) * ( sin x0))) / ( sin x0)) - ((( cos x1) * ( cos x1)) / ( sin x1))) / (x0 - x1)) by SIN_COS4: 5

      .= ((((1 / ( sin x0)) - ((( sin x0) * ( sin x0)) / ( sin x0))) - ((1 - (( sin x1) * ( sin x1))) / ( sin x1))) / (x0 - x1)) by SIN_COS4: 5

      .= ((((1 / ( sin x0)) - ( sin x0)) - ((1 / ( sin x1)) - ((( sin x1) * ( sin x1)) / ( sin x1)))) / (x0 - x1)) by A2, FDIFF_8: 2, XCMPLX_1: 89

      .= ((((1 / ( sin x0)) - ( sin x0)) - ((1 / ( sin x1)) - ( sin x1))) / (x0 - x1)) by A2, FDIFF_8: 2, XCMPLX_1: 89

      .= (((((1 / ( sin x0)) - ( sin x0)) - (1 / ( sin x1))) + ( sin x1)) / (x0 - x1));

      hence thesis;

    end;

    theorem :: DIFF_3:86

    (for x holds (f . x) = (( cot (#) cos ) . x)) & x in ( dom cot ) & (x + h) in ( dom cot ) implies (( fD (f,h)) . x) = ((((1 / ( sin (x + h))) - ( sin (x + h))) - (1 / ( sin x))) + ( sin x))

    proof

      assume that

       A1: for x holds (f . x) = (( cot (#) cos ) . x) and

       A2: x in ( dom cot ) & (x + h) in ( dom cot );

      (( fD (f,h)) . x) = ((f . (x + h)) - (f . x)) by DIFF_1: 3

      .= ((( cot (#) cos ) . (x + h)) - (f . x)) by A1

      .= ((( cot (#) cos ) . (x + h)) - (( cot (#) cos ) . x)) by A1

      .= ((( cot . (x + h)) * ( cos . (x + h))) - (( cot (#) cos ) . x)) by VALUED_1: 5

      .= ((( cot . (x + h)) * ( cos . (x + h))) - (( cot . x) * ( cos . x))) by VALUED_1: 5

      .= (((( cos . (x + h)) * (( sin . (x + h)) " )) * ( cos . (x + h))) - (( cot . x) * ( cos . x))) by A2, RFUNCT_1:def 1

      .= (((( cos (x + h)) / ( sin (x + h))) * ( cos (x + h))) - ((( cos x) / ( sin x)) * ( cos x))) by A2, RFUNCT_1:def 1

      .= ((( cos (x + h)) / (( sin (x + h)) / ( cos (x + h)))) - ((( cos x) / ( sin x)) * ( cos x))) by XCMPLX_1: 82

      .= ((( cos (x + h)) / (( sin (x + h)) / ( cos (x + h)))) - (( cos x) / (( sin x) / ( cos x)))) by XCMPLX_1: 82

      .= (((( cos (x + h)) * ( cos (x + h))) / ( sin (x + h))) - (( cos x) / (( sin x) / ( cos x)))) by XCMPLX_1: 77

      .= (((( cos (x + h)) * ( cos (x + h))) / ( sin (x + h))) - ((( cos x) * ( cos x)) / ( sin x))) by XCMPLX_1: 77

      .= (((1 - (( sin (x + h)) * ( sin (x + h)))) / ( sin (x + h))) - ((( cos x) * ( cos x)) / ( sin x))) by SIN_COS4: 5

      .= (((1 / ( sin (x + h))) - ((( sin (x + h)) * ( sin (x + h))) / ( sin (x + h)))) - ((1 - (( sin x) * ( sin x))) / ( sin x))) by SIN_COS4: 5

      .= (((1 / ( sin (x + h))) - ( sin (x + h))) - ((1 / ( sin x)) - ((( sin x) * ( sin x)) / ( sin x)))) by A2, FDIFF_8: 2, XCMPLX_1: 89

      .= (((1 / ( sin (x + h))) - ( sin (x + h))) - ((1 / ( sin x)) - ( sin x))) by A2, FDIFF_8: 2, XCMPLX_1: 89

      .= ((((1 / ( sin (x + h))) - ( sin (x + h))) - (1 / ( sin x))) + ( sin x));

      hence thesis;

    end;

    theorem :: DIFF_3:87

    (for x holds (f . x) = (( cot (#) cos ) . x)) & x in ( dom cot ) & (x - h) in ( dom cot ) implies (( bD (f,h)) . x) = ((((1 / ( sin x)) - ( sin x)) - (1 / ( sin (x - h)))) + ( sin (x - h)))

    proof

      assume that

       A1: for x holds (f . x) = (( cot (#) cos ) . x) and

       A2: x in ( dom cot ) & (x - h) in ( dom cot );

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((( cot (#) cos ) . x) - (f . (x - h))) by A1

      .= ((( cot (#) cos ) . x) - (( cot (#) cos ) . (x - h))) by A1

      .= ((( cot . x) * ( cos . x)) - (( cot (#) cos ) . (x - h))) by VALUED_1: 5

      .= ((( cot . x) * ( cos . x)) - (( cot . (x - h)) * ( cos . (x - h)))) by VALUED_1: 5

      .= (((( cos . x) * (( sin . x) " )) * ( cos . x)) - (( cot . (x - h)) * ( cos . (x - h)))) by A2, RFUNCT_1:def 1

      .= (((( cos x) / ( sin x)) * ( cos x)) - ((( cos (x - h)) / ( sin (x - h))) * ( cos (x - h)))) by A2, RFUNCT_1:def 1

      .= ((( cos x) / (( sin x) / ( cos x))) - ((( cos (x - h)) / ( sin (x - h))) * ( cos (x - h)))) by XCMPLX_1: 82

      .= ((( cos x) / (( sin x) / ( cos x))) - (( cos (x - h)) / (( sin (x - h)) / ( cos (x - h))))) by XCMPLX_1: 82

      .= (((( cos x) * ( cos x)) / ( sin x)) - (( cos (x - h)) / (( sin (x - h)) / ( cos (x - h))))) by XCMPLX_1: 77

      .= (((( cos x) * ( cos x)) / ( sin x)) - ((( cos (x - h)) * ( cos (x - h))) / ( sin (x - h)))) by XCMPLX_1: 77

      .= (((1 - (( sin x) * ( sin x))) / ( sin x)) - ((( cos (x - h)) * ( cos (x - h))) / ( sin (x - h)))) by SIN_COS4: 5

      .= (((1 / ( sin x)) - ((( sin x) * ( sin x)) / ( sin x))) - ((1 - (( sin (x - h)) * ( sin (x - h)))) / ( sin (x - h)))) by SIN_COS4: 5

      .= (((1 / ( sin x)) - ( sin x)) - ((1 / ( sin (x - h))) - ((( sin (x - h)) * ( sin (x - h))) / ( sin (x - h))))) by A2, FDIFF_8: 2, XCMPLX_1: 89

      .= (((1 / ( sin x)) - ( sin x)) - ((1 / ( sin (x - h))) - ( sin (x - h)))) by A2, FDIFF_8: 2, XCMPLX_1: 89

      .= ((((1 / ( sin x)) - ( sin x)) - (1 / ( sin (x - h)))) + ( sin (x - h)));

      hence thesis;

    end;

    theorem :: DIFF_3:88

    (for x holds (f . x) = (( cot (#) cos ) . x)) & (x + (h / 2)) in ( dom cot ) & (x - (h / 2)) in ( dom cot ) implies (( cD (f,h)) . x) = ((((1 / ( sin (x + (h / 2)))) - ( sin (x + (h / 2)))) - (1 / ( sin (x - (h / 2))))) + ( sin (x - (h / 2))))

    proof

      assume that

       A1: for x holds (f . x) = (( cot (#) cos ) . x) and

       A2: (x + (h / 2)) in ( dom cot ) & (x - (h / 2)) in ( dom cot );

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= ((( cot (#) cos ) . (x + (h / 2))) - (f . (x - (h / 2)))) by A1

      .= ((( cot (#) cos ) . (x + (h / 2))) - (( cot (#) cos ) . (x - (h / 2)))) by A1

      .= ((( cot . (x + (h / 2))) * ( cos . (x + (h / 2)))) - (( cot (#) cos ) . (x - (h / 2)))) by VALUED_1: 5

      .= ((( cot . (x + (h / 2))) * ( cos . (x + (h / 2)))) - (( cot . (x - (h / 2))) * ( cos . (x - (h / 2))))) by VALUED_1: 5

      .= (((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * ( cos . (x + (h / 2)))) - (( cot . (x - (h / 2))) * ( cos . (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= (((( cos (x + (h / 2))) / ( sin (x + (h / 2)))) * ( cos (x + (h / 2)))) - ((( cos (x - (h / 2))) / ( sin (x - (h / 2)))) * ( cos (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= ((( cos (x + (h / 2))) / (( sin (x + (h / 2))) / ( cos (x + (h / 2))))) - ((( cos (x - (h / 2))) / ( sin (x - (h / 2)))) * ( cos (x - (h / 2))))) by XCMPLX_1: 82

      .= ((( cos (x + (h / 2))) / (( sin (x + (h / 2))) / ( cos (x + (h / 2))))) - (( cos (x - (h / 2))) / (( sin (x - (h / 2))) / ( cos (x - (h / 2)))))) by XCMPLX_1: 82

      .= (((( cos (x + (h / 2))) * ( cos (x + (h / 2)))) / ( sin (x + (h / 2)))) - (( cos (x - (h / 2))) / (( sin (x - (h / 2))) / ( cos (x - (h / 2)))))) by XCMPLX_1: 77

      .= (((( cos (x + (h / 2))) * ( cos (x + (h / 2)))) / ( sin (x + (h / 2)))) - ((( cos (x - (h / 2))) * ( cos (x - (h / 2)))) / ( sin (x - (h / 2))))) by XCMPLX_1: 77

      .= (((1 - (( sin (x + (h / 2))) * ( sin (x + (h / 2))))) / ( sin (x + (h / 2)))) - ((( cos (x - (h / 2))) * ( cos (x - (h / 2)))) / ( sin (x - (h / 2))))) by SIN_COS4: 5

      .= (((1 / ( sin (x + (h / 2)))) - ((( sin (x + (h / 2))) * ( sin (x + (h / 2)))) / ( sin (x + (h / 2))))) - ((1 - (( sin (x - (h / 2))) * ( sin (x - (h / 2))))) / ( sin (x - (h / 2))))) by SIN_COS4: 5

      .= (((1 / ( sin (x + (h / 2)))) - ( sin (x + (h / 2)))) - ((1 / ( sin (x - (h / 2)))) - ((( sin (x - (h / 2))) * ( sin (x - (h / 2)))) / ( sin (x - (h / 2)))))) by A2, FDIFF_8: 2, XCMPLX_1: 89

      .= (((1 / ( sin (x + (h / 2)))) - ( sin (x + (h / 2)))) - ((1 / ( sin (x - (h / 2)))) - ( sin (x - (h / 2))))) by A2, FDIFF_8: 2, XCMPLX_1: 89

      .= ((((1 / ( sin (x + (h / 2)))) - ( sin (x + (h / 2)))) - (1 / ( sin (x - (h / 2))))) + ( sin (x - (h / 2))));

      hence thesis;

    end;

    theorem :: DIFF_3:89

    (for x holds (f . x) = (( cot (#) sin ) . x)) & x0 in ( dom cot ) & x1 in ( dom cot ) implies [!f, x0, x1!] = ((( cos x0) - ( cos x1)) / (x0 - x1))

    proof

      assume that

       A1: for x holds (f . x) = (( cot (#) sin ) . x) and

       A2: x0 in ( dom cot ) & x1 in ( dom cot );

      

       A3: (f . x0) = (( cot (#) sin ) . x0) by A1;

      (f . x1) = (( cot (#) sin ) . x1) by A1;

      

      then [!f, x0, x1!] = (((( cot . x0) * ( sin . x0)) - (( cot (#) sin ) . x1)) / (x0 - x1)) by A3, VALUED_1: 5

      .= (((( cot . x0) * ( sin . x0)) - (( cot . x1) * ( sin . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cos . x0) * (( sin . x0) " )) * ( sin . x0)) - (( cot . x1) * ( sin . x1))) / (x0 - x1)) by A2, RFUNCT_1:def 1

      .= ((((( cos x0) / ( sin x0)) * ( sin x0)) - ((( cos x1) / ( sin x1)) * ( sin x1))) / (x0 - x1)) by A2, RFUNCT_1:def 1

      .= (((( cos x0) / (( sin x0) / ( sin x0))) - ((( cos x1) / ( sin x1)) * ( sin x1))) / (x0 - x1)) by XCMPLX_1: 82

      .= (((( cos x0) / (( sin x0) * (1 / ( sin x0)))) - (( cos x1) / (( sin x1) / ( sin x1)))) / (x0 - x1)) by XCMPLX_1: 82

      .= (((( cos x0) / 1) - (( cos x1) / (( sin x1) * (1 / ( sin x1))))) / (x0 - x1)) by A2, FDIFF_8: 2, XCMPLX_1: 106

      .= (((( cos x0) / 1) - (( cos x1) / 1)) / (x0 - x1)) by A2, FDIFF_8: 2, XCMPLX_1: 106

      .= ((( cos x0) - ( cos x1)) / (x0 - x1));

      hence thesis;

    end;

    theorem :: DIFF_3:90

    (for x holds (f . x) = (( cot (#) sin ) . x)) & x in ( dom cot ) & (x + h) in ( dom cot ) implies (( fD (f,h)) . x) = (( cos (x + h)) - ( cos x))

    proof

      assume that

       A1: for x holds (f . x) = (( cot (#) sin ) . x) and

       A2: x in ( dom cot ) & (x + h) in ( dom cot );

      (( fD (f,h)) . x) = ((f . (x + h)) - (f . x)) by DIFF_1: 3

      .= ((( cot (#) sin ) . (x + h)) - (f . x)) by A1

      .= ((( cot (#) sin ) . (x + h)) - (( cot (#) sin ) . x)) by A1

      .= ((( cot . (x + h)) * ( sin . (x + h))) - (( cot (#) sin ) . x)) by VALUED_1: 5

      .= ((( cot . (x + h)) * ( sin . (x + h))) - (( cot . x) * ( sin . x))) by VALUED_1: 5

      .= (((( cos . (x + h)) * (( sin . (x + h)) " )) * ( sin . (x + h))) - (( cot . x) * ( sin . x))) by A2, RFUNCT_1:def 1

      .= (((( cos (x + h)) / ( sin (x + h))) * ( sin (x + h))) - ((( cos x) / ( sin x)) * ( sin x))) by A2, RFUNCT_1:def 1

      .= ((( cos (x + h)) / (( sin (x + h)) / ( sin (x + h)))) - ((( cos x) / ( sin x)) * ( sin x))) by XCMPLX_1: 82

      .= ((( cos (x + h)) / (( sin (x + h)) * (1 / ( sin (x + h))))) - (( cos x) / (( sin x) / ( sin x)))) by XCMPLX_1: 82

      .= ((( cos (x + h)) / 1) - (( cos x) / (( sin x) * (1 / ( sin x))))) by A2, FDIFF_8: 2, XCMPLX_1: 106

      .= ((( cos (x + h)) / 1) - (( cos x) / 1)) by A2, FDIFF_8: 2, XCMPLX_1: 106

      .= (( cos (x + h)) - ( cos x));

      hence thesis;

    end;

    theorem :: DIFF_3:91

    (for x holds (f . x) = (( cot (#) sin ) . x)) & x in ( dom cot ) & (x - h) in ( dom cot ) implies (( bD (f,h)) . x) = (( cos x) - ( cos (x - h)))

    proof

      assume that

       A1: for x holds (f . x) = (( cot (#) sin ) . x) and

       A2: x in ( dom cot ) & (x - h) in ( dom cot );

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((( cot (#) sin ) . x) - (f . (x - h))) by A1

      .= ((( cot (#) sin ) . x) - (( cot (#) sin ) . (x - h))) by A1

      .= ((( cot . x) * ( sin . x)) - (( cot (#) sin ) . (x - h))) by VALUED_1: 5

      .= ((( cot . x) * ( sin . x)) - (( cot . (x - h)) * ( sin . (x - h)))) by VALUED_1: 5

      .= (((( cos . x) * (( sin . x) " )) * ( sin . x)) - (( cot . (x - h)) * ( sin . (x - h)))) by A2, RFUNCT_1:def 1

      .= (((( cos x) / ( sin x)) * ( sin x)) - ((( cos (x - h)) / ( sin (x - h))) * ( sin (x - h)))) by A2, RFUNCT_1:def 1

      .= ((( cos x) / (( sin x) / ( sin x))) - ((( cos (x - h)) / ( sin (x - h))) * ( sin (x - h)))) by XCMPLX_1: 82

      .= ((( cos x) / (( sin x) * (1 / ( sin x)))) - (( cos (x - h)) / (( sin (x - h)) / ( sin (x - h))))) by XCMPLX_1: 82

      .= ((( cos x) / 1) - (( cos (x - h)) / (( sin (x - h)) * (1 / ( sin (x - h)))))) by A2, FDIFF_8: 2, XCMPLX_1: 106

      .= ((( cos x) / 1) - (( cos (x - h)) / 1)) by A2, FDIFF_8: 2, XCMPLX_1: 106

      .= (( cos x) - ( cos (x - h)));

      hence thesis;

    end;

    theorem :: DIFF_3:92

    (for x holds (f . x) = (( cot (#) sin ) . x)) & (x + (h / 2)) in ( dom cot ) & (x - (h / 2)) in ( dom cot ) implies (( cD (f,h)) . x) = (( cos (x + (h / 2))) - ( cos (x - (h / 2))))

    proof

      assume that

       A1: for x holds (f . x) = (( cot (#) sin ) . x) and

       A2: (x + (h / 2)) in ( dom cot ) & (x - (h / 2)) in ( dom cot );

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= ((( cot (#) sin ) . (x + (h / 2))) - (f . (x - (h / 2)))) by A1

      .= ((( cot (#) sin ) . (x + (h / 2))) - (( cot (#) sin ) . (x - (h / 2)))) by A1

      .= ((( cot . (x + (h / 2))) * ( sin . (x + (h / 2)))) - (( cot (#) sin ) . (x - (h / 2)))) by VALUED_1: 5

      .= ((( cot . (x + (h / 2))) * ( sin . (x + (h / 2)))) - (( cot . (x - (h / 2))) * ( sin . (x - (h / 2))))) by VALUED_1: 5

      .= (((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * ( sin . (x + (h / 2)))) - (( cot . (x - (h / 2))) * ( sin . (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= (((( cos (x + (h / 2))) / ( sin (x + (h / 2)))) * ( sin (x + (h / 2)))) - ((( cos (x - (h / 2))) / ( sin (x - (h / 2)))) * ( sin (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= ((( cos (x + (h / 2))) / (( sin (x + (h / 2))) / ( sin (x + (h / 2))))) - ((( cos (x - (h / 2))) / ( sin (x - (h / 2)))) * ( sin (x - (h / 2))))) by XCMPLX_1: 82

      .= ((( cos (x + (h / 2))) / (( sin (x + (h / 2))) * (1 / ( sin (x + (h / 2)))))) - (( cos (x - (h / 2))) / (( sin (x - (h / 2))) / ( sin (x - (h / 2)))))) by XCMPLX_1: 82

      .= ((( cos (x + (h / 2))) / 1) - (( cos (x - (h / 2))) / (( sin (x - (h / 2))) * (1 / ( sin (x - (h / 2))))))) by A2, FDIFF_8: 2, XCMPLX_1: 106

      .= ((( cos (x + (h / 2))) / 1) - (( cos (x - (h / 2))) / 1)) by A2, FDIFF_8: 2, XCMPLX_1: 106

      .= (( cos (x + (h / 2))) - ( cos (x - (h / 2))));

      hence thesis;

    end;

    theorem :: DIFF_3:93

    (for x holds (f . x) = (( tan (#) tan ) . x)) & x0 in ( dom tan ) & x1 in ( dom tan ) implies [!f, x0, x1!] = (((( cos x1) ^2 ) - (( cos x0) ^2 )) / (((( cos x0) * ( cos x1)) ^2 ) * (x0 - x1)))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) tan ) . x) and

       A2: x0 in ( dom tan ) & x1 in ( dom tan );

      

       A3: ( cos x0) <> 0 & ( cos x1) <> 0 by A2, FDIFF_8: 1;

      

       A4: (f . x0) = (( tan (#) tan ) . x0) by A1;

      (f . x1) = (( tan (#) tan ) . x1) by A1;

      

      then [!f, x0, x1!] = (((( tan . x0) * ( tan . x0)) - (( tan (#) tan ) . x1)) / (x0 - x1)) by A4, VALUED_1: 5

      .= (((( tan . x0) * ( tan . x0)) - (( tan . x1) * ( tan . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( sin . x0) * (( cos . x0) " )) * ( tan . x0)) - (( tan . x1) * ( tan . x1))) / (x0 - x1)) by A2, RFUNCT_1:def 1

      .= ((((( sin . x0) * (( cos . x0) " )) * (( sin . x0) * (( cos . x0) " ))) - (( tan . x1) * ( tan . x1))) / (x0 - x1)) by A2, RFUNCT_1:def 1

      .= ((((( sin . x0) * (( cos . x0) " )) * (( sin . x0) * (( cos . x0) " ))) - ((( sin . x1) * (( cos . x1) " )) * ( tan . x1))) / (x0 - x1)) by A2, RFUNCT_1:def 1

      .= (((( tan x0) ^2 ) - (( tan x1) ^2 )) / (x0 - x1)) by A2, RFUNCT_1:def 1

      .= (((( tan x0) - ( tan x1)) * (( tan x0) + ( tan x1))) / (x0 - x1))

      .= (((( sin (x0 - x1)) / (( cos x0) * ( cos x1))) * (( tan x0) + ( tan x1))) / (x0 - x1)) by A3, SIN_COS4: 20

      .= (((( sin (x0 - x1)) / (( cos x0) * ( cos x1))) * (( sin (x0 + x1)) / (( cos x0) * ( cos x1)))) / (x0 - x1)) by A3, SIN_COS4: 19

      .= (((( sin (x0 + x1)) * ( sin (x0 - x1))) / ((( cos x0) * ( cos x1)) ^2 )) / (x0 - x1)) by XCMPLX_1: 76

      .= ((((( cos x1) ^2 ) - (( cos x0) ^2 )) / ((( cos x0) * ( cos x1)) ^2 )) / (x0 - x1)) by SIN_COS4: 38

      .= (((( cos x1) ^2 ) - (( cos x0) ^2 )) / (((( cos x0) * ( cos x1)) ^2 ) * (x0 - x1))) by XCMPLX_1: 78;

      hence thesis;

    end;

    theorem :: DIFF_3:94

    (for x holds (f . x) = (( tan (#) tan ) . x)) & x in ( dom tan ) & (x + h) in ( dom tan ) implies (( fD (f,h)) . x) = ( - (((1 / 2) * (( cos (2 * (x + h))) - ( cos (2 * x)))) / ((( cos (x + h)) * ( cos x)) ^2 )))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) tan ) . x) and

       A2: x in ( dom tan ) & (x + h) in ( dom tan );

      

       A3: ( cos x) <> 0 & ( cos (x + h)) <> 0 by A2, FDIFF_8: 1;

      (( fD (f,h)) . x) = ((f . (x + h)) - (f . x)) by DIFF_1: 3

      .= ((( tan (#) tan ) . (x + h)) - (f . x)) by A1

      .= ((( tan (#) tan ) . (x + h)) - (( tan (#) tan ) . x)) by A1

      .= ((( tan . (x + h)) * ( tan . (x + h))) - (( tan (#) tan ) . x)) by VALUED_1: 5

      .= ((( tan . (x + h)) * ( tan . (x + h))) - (( tan . x) * ( tan . x))) by VALUED_1: 5

      .= (((( sin . (x + h)) * (( cos . (x + h)) " )) * ( tan . (x + h))) - (( tan . x) * ( tan . x))) by A2, RFUNCT_1:def 1

      .= (((( sin . (x + h)) * (( cos . (x + h)) " )) * (( sin . (x + h)) * (( cos . (x + h)) " ))) - (( tan . x) * ( tan . x))) by A2, RFUNCT_1:def 1

      .= (((( sin . (x + h)) * (( cos . (x + h)) " )) * (( sin . (x + h)) * (( cos . (x + h)) " ))) - ((( sin . x) * (( cos . x) " )) * ( tan . x))) by A2, RFUNCT_1:def 1

      .= ((( tan (x + h)) ^2 ) - (( tan x) ^2 )) by A2, RFUNCT_1:def 1

      .= ((( tan (x + h)) - ( tan x)) * (( tan (x + h)) + ( tan x)))

      .= ((( sin ((x + h) - x)) / (( cos (x + h)) * ( cos x))) * (( tan (x + h)) + ( tan x))) by A3, SIN_COS4: 20

      .= ((( sin ((x + h) - x)) / (( cos (x + h)) * ( cos x))) * (( sin ((x + h) + x)) / (( cos (x + h)) * ( cos x)))) by A3, SIN_COS4: 19

      .= ((( sin ((2 * x) + h)) * ( sin h)) / ((( cos (x + h)) * ( cos x)) ^2 )) by XCMPLX_1: 76

      .= (( - ((1 / 2) * (( cos (((2 * x) + h) + h)) - ( cos (((2 * x) + h) - h))))) / ((( cos (x + h)) * ( cos x)) ^2 )) by SIN_COS4: 29

      .= ( - (((1 / 2) * (( cos (2 * (x + h))) - ( cos (2 * x)))) / ((( cos (x + h)) * ( cos x)) ^2 )));

      hence thesis;

    end;

    theorem :: DIFF_3:95

    (for x holds (f . x) = (( tan (#) tan ) . x)) & x in ( dom tan ) & (x - h) in ( dom tan ) implies (( bD (f,h)) . x) = ( - (((1 / 2) * (( cos (2 * x)) - ( cos (2 * (h - x))))) / ((( cos x) * ( cos (x - h))) ^2 )))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) tan ) . x) and

       A2: x in ( dom tan ) & (x - h) in ( dom tan );

      

       A3: ( cos x) <> 0 & ( cos (x - h)) <> 0 by A2, FDIFF_8: 1;

      (( bD (f,h)) . x) = ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= ((( tan (#) tan ) . x) - (f . (x - h))) by A1

      .= ((( tan (#) tan ) . x) - (( tan (#) tan ) . (x - h))) by A1

      .= ((( tan . x) * ( tan . x)) - (( tan (#) tan ) . (x - h))) by VALUED_1: 5

      .= ((( tan . x) * ( tan . x)) - (( tan . (x - h)) * ( tan . (x - h)))) by VALUED_1: 5

      .= (((( sin . x) * (( cos . x) " )) * ( tan . x)) - (( tan . (x - h)) * ( tan . (x - h)))) by A2, RFUNCT_1:def 1

      .= (((( sin . x) * (( cos . x) " )) * (( sin . x) * (( cos . x) " ))) - (( tan . (x - h)) * ( tan . (x - h)))) by A2, RFUNCT_1:def 1

      .= (((( sin . x) * (( cos . x) " )) * (( sin . x) * (( cos . x) " ))) - ((( sin . (x - h)) * (( cos . (x - h)) " )) * ( tan . (x - h)))) by A2, RFUNCT_1:def 1

      .= ((( tan x) ^2 ) - (( tan (x - h)) ^2 )) by A2, RFUNCT_1:def 1

      .= ((( tan x) - ( tan (x - h))) * (( tan x) + ( tan (x - h))))

      .= ((( sin (x - (x - h))) / (( cos x) * ( cos (x - h)))) * (( tan x) + ( tan (x - h)))) by A3, SIN_COS4: 20

      .= ((( sin h) / (( cos x) * ( cos (x - h)))) * (( sin (x + (x - h))) / (( cos x) * ( cos (x - h))))) by A3, SIN_COS4: 19

      .= ((( sin h) * ( sin ((2 * x) - h))) / ((( cos x) * ( cos (x - h))) ^2 )) by XCMPLX_1: 76

      .= (( - ((1 / 2) * (( cos (h + ((2 * x) - h))) - ( cos (h - ((2 * x) - h)))))) / ((( cos x) * ( cos (x - h))) ^2 )) by SIN_COS4: 29

      .= ( - (((1 / 2) * (( cos (2 * x)) - ( cos (2 * (h - x))))) / ((( cos x) * ( cos (x - h))) ^2 )));

      hence thesis;

    end;

    theorem :: DIFF_3:96

    (for x holds (f . x) = (( tan (#) tan ) . x)) & (x + (h / 2)) in ( dom tan ) & (x - (h / 2)) in ( dom tan ) implies (( cD (f,h)) . x) = ( - (((1 / 2) * (( cos (h + (2 * x))) - ( cos (h - (2 * x))))) / ((( cos (x + (h / 2))) * ( cos (x - (h / 2)))) ^2 )))

    proof

      assume that

       A1: for x holds (f . x) = (( tan (#) tan ) . x) and

       A2: (x + (h / 2)) in ( dom tan ) & (x - (h / 2)) in ( dom tan );

      

       A3: ( cos (x + (h / 2))) <> 0 & ( cos (x - (h / 2))) <> 0 by A2, FDIFF_8: 1;

      (( cD (f,h)) . x) = ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= ((( tan (#) tan ) . (x + (h / 2))) - (f . (x - (h / 2)))) by A1

      .= ((( tan (#) tan ) . (x + (h / 2))) - (( tan (#) tan ) . (x - (h / 2)))) by A1

      .= ((( tan . (x + (h / 2))) * ( tan . (x + (h / 2)))) - (( tan (#) tan ) . (x - (h / 2)))) by VALUED_1: 5

      .= ((( tan . (x + (h / 2))) * ( tan . (x + (h / 2)))) - (( tan . (x - (h / 2))) * ( tan . (x - (h / 2))))) by VALUED_1: 5

      .= (((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * ( tan . (x + (h / 2)))) - (( tan . (x - (h / 2))) * ( tan . (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= (((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * (( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " ))) - (( tan . (x - (h / 2))) * ( tan . (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= (((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * (( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " ))) - ((( sin . (x - (h / 2))) * (( cos . (x - (h / 2))) " )) * ( tan . (x - (h / 2))))) by A2, RFUNCT_1:def 1

      .= ((( tan (x + (h / 2))) ^2 ) - (( tan (x - (h / 2))) ^2 )) by A2, RFUNCT_1:def 1

      .= ((( tan (x + (h / 2))) - ( tan (x - (h / 2)))) * (( tan (x + (h / 2))) + ( tan (x - (h / 2)))))

      .= ((( sin ((x + (h / 2)) - (x - (h / 2)))) / (( cos (x + (h / 2))) * ( cos (x - (h / 2))))) * (( tan (x + (h / 2))) + ( tan (x - (h / 2))))) by A3, SIN_COS4: 20

      .= ((( sin h) / (( cos (x + (h / 2))) * ( cos (x - (h / 2))))) * (( sin ((x + (h / 2)) + (x - (h / 2)))) / (( cos (x + (h / 2))) * ( cos (x - (h / 2)))))) by A3, SIN_COS4: 19

      .= ((( sin h) * ( sin (2 * x))) / ((( cos (x + (h / 2))) * ( cos (x - (h / 2)))) ^2 )) by XCMPLX_1: 76

      .= (( - ((1 / 2) * (( cos (h + (2 * x))) - ( cos (h - (2 * x)))))) / ((( cos (x + (h / 2))) * ( cos (x - (h / 2)))) ^2 )) by SIN_COS4: 29

      .= ( - (((1 / 2) * (( cos (h + (2 * x))) - ( cos (h - (2 * x))))) / ((( cos (x + (h / 2))) * ( cos (x - (h / 2)))) ^2 )));

      hence thesis;

    end;