diff_2.miz



    begin

    reserve h,r,r1,r2,x0,x1,x2,x3,x4,x5,x,a,b,c,k for Real,

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

    theorem :: DIFF_2:1

    

     Th1: [!f, x, (x + h)!] = (((( fdif (f,h)) . 1) . x) / h)

    proof

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

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

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

      .= (((( fdif (f,h)) . ( 0 qua Nat + 1)) . x) / h) by DIFF_1:def 6;

      hence thesis;

    end;

    theorem :: DIFF_2:2

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

    proof

      

       A1: (( fdif (f,h)) . 1) is Function of REAL , REAL by DIFF_1: 2;

      assume

       A2: h <> 0 ;

      then

       A3: (x + h) <> (x + (2 * h));

      x <> (x + h) & x <> (x + (2 * h)) by A2;

      then (x,(x + h),(x + (2 * h))) are_mutually_distinct by A3, ZFMISC_1:def 5;

      

      then [!f, x, (x + h), (x + (2 * h))!] = [!f, (x + (2 * h)), (x + h), x!] by DIFF_1: 34

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

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

      .= (((((( fdif (f,h)) . 1) . (x + h)) / h) - [!f, x, (x + h)!]) / ((x + (2 * h)) - x)) by Th1

      .= (((((( fdif (f,h)) . 1) . (x + h)) / h) - (((( fdif (f,h)) . 1) . x) / h)) / ((x + (2 * h)) - x)) by Th1

      .= (((((( fdif (f,h)) . 1) . (x + h)) - ((( fdif (f,h)) . 1) . x)) / h) / ((x + (2 * h)) - x)) by XCMPLX_1: 120

      .= (((( fD ((( fdif (f,h)) . 1),h)) . x) / h) / (2 * h)) by A1, DIFF_1: 3

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

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

      .= (((( fdif (f,h)) . 2) . x) / (2 * (h ^2 )));

      hence thesis;

    end;

    theorem :: DIFF_2:3

    

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

    proof

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

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

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

      .= (((( bdif (f,h)) . ( 0 qua Nat + 1)) . x) / h) by DIFF_1:def 7;

      hence thesis;

    end;

    theorem :: DIFF_2:4

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

    proof

      set y = (x - h);

      

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

      assume

       A2: h <> 0 ;

      then

       A3: (x - h) <> (x - (2 * h));

      x <> (x - h) & x <> (x - (2 * h)) by A2;

      then (x,(x - h),(x - (2 * h))) are_mutually_distinct by A3, ZFMISC_1:def 5;

      

      then [!f, (x - (2 * h)), (x - h), x!] = [!f, x, (x - h), (x - (2 * h))!] by DIFF_1: 34

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

      .= (((((( bdif (f,h)) . 1) . x) / h) - [!f, (x - h), (x - (2 * h))!]) / (x - (x - (2 * h)))) by Th3

      .= (((((( bdif (f,h)) . 1) . x) / h) - [!f, (y - h), y!]) / (x - (x - (2 * h)))) by DIFF_1: 29

      .= (((((( bdif (f,h)) . 1) . x) / h) - (((( bdif (f,h)) . 1) . (x - h)) / h)) / (x - (x - (2 * h)))) by Th3

      .= (((((( bdif (f,h)) . 1) . x) - ((( bdif (f,h)) . 1) . (x - h))) / h) / (x - (x - (2 * h)))) by XCMPLX_1: 120

      .= (((( bD ((( bdif (f,h)) . 1),h)) . x) / h) / (2 * h)) by A1, DIFF_1: 4

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

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

      .= (((( bdif (f,h)) . 2) . x) / (2 * (h ^2 )));

      hence thesis;

    end;

    theorem :: DIFF_2:5

    

     Th5: [!(r (#) f), x0, x1, x2!] = (r * [!f, x0, x1, x2!])

    proof

       [!(r (#) f), x0, x1, x2!] = (((r * [!f, x0, x1!]) - [!(r (#) f), x1, x2!]) / (x0 - x2)) by DIFF_1: 31

      .= (((r * [!f, x0, x1!]) - (r * [!f, x1, x2!])) / (x0 - x2)) by DIFF_1: 31

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

      hence thesis by XCMPLX_1: 74;

    end;

    theorem :: DIFF_2:6

    

     Th6: [!(f1 + f2), x0, x1, x2!] = ( [!f1, x0, x1, x2!] + [!f2, x0, x1, x2!])

    proof

       [!(f1 + f2), x0, x1, x2!] = ((( [!f1, x0, x1!] + [!f2, x0, x1!]) - [!(f1 + f2), x1, x2!]) / (x0 - x2)) by DIFF_1: 32

      .= ((( [!f1, x0, x1!] + [!f2, x0, x1!]) - ( [!f1, x1, x2!] + [!f2, x1, x2!])) / (x0 - x2)) by DIFF_1: 32

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

      hence thesis by XCMPLX_1: 62;

    end;

    theorem :: DIFF_2:7

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

    proof

       [!((r1 (#) f1) + (r2 (#) f2)), x0, x1, x2!] = ( [!(r1 (#) f1), x0, x1, x2!] + [!(r2 (#) f2), x0, x1, x2!]) by Th6

      .= ((r1 * [!f1, x0, x1, x2!]) + [!(r2 (#) f2), x0, x1, x2!]) by Th5;

      hence thesis by Th5;

    end;

    theorem :: DIFF_2:8

    

     Th8: [!(r (#) f), x0, x1, x2, x3!] = (r * [!f, x0, x1, x2, x3!])

    proof

       [!(r (#) f), x0, x1, x2, x3!] = (((r * [!f, x0, x1, x2!]) - [!(r (#) f), x1, x2, x3!]) / (x0 - x3)) by Th5

      .= (((r * [!f, x0, x1, x2!]) - (r * [!f, x1, x2, x3!])) / (x0 - x3)) by Th5

      .= ((r * ( [!f, x0, x1, x2!] - [!f, x1, x2, x3!])) / (x0 - x3));

      hence thesis by XCMPLX_1: 74;

    end;

    theorem :: DIFF_2:9

    

     Th9: [!(f1 + f2), x0, x1, x2, x3!] = ( [!f1, x0, x1, x2, x3!] + [!f2, x0, x1, x2, x3!])

    proof

       [!(f1 + f2), x0, x1, x2, x3!] = ((( [!f1, x0, x1, x2!] + [!f2, x0, x1, x2!]) - [!(f1 + f2), x1, x2, x3!]) / (x0 - x3)) by Th6

      .= ((( [!f1, x0, x1, x2!] + [!f2, x0, x1, x2!]) - ( [!f1, x1, x2, x3!] + [!f2, x1, x2, x3!])) / (x0 - x3)) by Th6

      .= ((( [!f1, x0, x1, x2!] - [!f1, x1, x2, x3!]) + ( [!f2, x0, x1, x2!] - [!f2, x1, x2, x3!])) / (x0 - x3));

      hence thesis by XCMPLX_1: 62;

    end;

    theorem :: DIFF_2:10

     [!((r1 (#) f1) + (r2 (#) f2)), x0, x1, x2, x3!] = ((r1 * [!f1, x0, x1, x2, x3!]) + (r2 * [!f2, x0, x1, x2, x3!]))

    proof

       [!((r1 (#) f1) + (r2 (#) f2)), x0, x1, x2, x3!] = ( [!(r1 (#) f1), x0, x1, x2, x3!] + [!(r2 (#) f2), x0, x1, x2, x3!]) by Th9

      .= ((r1 * [!f1, x0, x1, x2, x3!]) + [!(r2 (#) f2), x0, x1, x2, x3!]) by Th8;

      hence thesis by Th8;

    end;

    definition

      let f be real-valued Function;

      let x0,x1,x2,x3,x4 be Real;

      :: DIFF_2:def1

      func [!f,x0,x1,x2,x3,x4!] -> Real equals (( [!f, x0, x1, x2, x3!] - [!f, x1, x2, x3, x4!]) / (x0 - x4));

      correctness ;

    end

    theorem :: DIFF_2:11

    

     Th11: [!(r (#) f), x0, x1, x2, x3, x4!] = (r * [!f, x0, x1, x2, x3, x4!])

    proof

       [!(r (#) f), x0, x1, x2, x3, x4!] = (((r * [!f, x0, x1, x2, x3!]) - [!(r (#) f), x1, x2, x3, x4!]) / (x0 - x4)) by Th8

      .= (((r * [!f, x0, x1, x2, x3!]) - (r * [!f, x1, x2, x3, x4!])) / (x0 - x4)) by Th8

      .= ((r * ( [!f, x0, x1, x2, x3!] - [!f, x1, x2, x3, x4!])) / (x0 - x4));

      hence thesis by XCMPLX_1: 74;

    end;

    theorem :: DIFF_2:12

    

     Th12: [!(f1 + f2), x0, x1, x2, x3, x4!] = ( [!f1, x0, x1, x2, x3, x4!] + [!f2, x0, x1, x2, x3, x4!])

    proof

       [!(f1 + f2), x0, x1, x2, x3, x4!] = ((( [!f1, x0, x1, x2, x3!] + [!f2, x0, x1, x2, x3!]) - [!(f1 + f2), x1, x2, x3, x4!]) / (x0 - x4)) by Th9

      .= ((( [!f1, x0, x1, x2, x3!] + [!f2, x0, x1, x2, x3!]) - ( [!f1, x1, x2, x3, x4!] + [!f2, x1, x2, x3, x4!])) / (x0 - x4)) by Th9

      .= ((( [!f1, x0, x1, x2, x3!] - [!f1, x1, x2, x3, x4!]) + ( [!f2, x0, x1, x2, x3!] - [!f2, x1, x2, x3, x4!])) / (x0 - x4));

      hence thesis by XCMPLX_1: 62;

    end;

    theorem :: DIFF_2:13

     [!((r1 (#) f1) + (r2 (#) f2)), x0, x1, x2, x3, x4!] = ((r1 * [!f1, x0, x1, x2, x3, x4!]) + (r2 * [!f2, x0, x1, x2, x3, x4!]))

    proof

       [!((r1 (#) f1) + (r2 (#) f2)), x0, x1, x2, x3, x4!] = ( [!(r1 (#) f1), x0, x1, x2, x3, x4!] + [!(r2 (#) f2), x0, x1, x2, x3, x4!]) by Th12

      .= ((r1 * [!f1, x0, x1, x2, x3, x4!]) + [!(r2 (#) f2), x0, x1, x2, x3, x4!]) by Th11;

      hence thesis by Th11;

    end;

    definition

      let f be real-valued Function;

      let x0,x1,x2,x3,x4,x5 be Real;

      :: DIFF_2:def2

      func [!f,x0,x1,x2,x3,x4,x5!] -> Real equals (( [!f, x0, x1, x2, x3, x4!] - [!f, x1, x2, x3, x4, x5!]) / (x0 - x5));

      correctness ;

    end

    theorem :: DIFF_2:14

    

     Th14: [!(r (#) f), x0, x1, x2, x3, x4, x5!] = (r * [!f, x0, x1, x2, x3, x4, x5!])

    proof

       [!(r (#) f), x0, x1, x2, x3, x4, x5!] = (((r * [!f, x0, x1, x2, x3, x4!]) - [!(r (#) f), x1, x2, x3, x4, x5!]) / (x0 - x5)) by Th11

      .= (((r * [!f, x0, x1, x2, x3, x4!]) - (r * [!f, x1, x2, x3, x4, x5!])) / (x0 - x5)) by Th11

      .= ((r * ( [!f, x0, x1, x2, x3, x4!] - [!f, x1, x2, x3, x4, x5!])) / (x0 - x5));

      hence thesis by XCMPLX_1: 74;

    end;

    theorem :: DIFF_2:15

    

     Th15: [!(f1 + f2), x0, x1, x2, x3, x4, x5!] = ( [!f1, x0, x1, x2, x3, x4, x5!] + [!f2, x0, x1, x2, x3, x4, x5!])

    proof

       [!(f1 + f2), x0, x1, x2, x3, x4, x5!] = ((( [!f1, x0, x1, x2, x3, x4!] + [!f2, x0, x1, x2, x3, x4!]) - [!(f1 + f2), x1, x2, x3, x4, x5!]) / (x0 - x5)) by Th12

      .= ((( [!f1, x0, x1, x2, x3, x4!] + [!f2, x0, x1, x2, x3, x4!]) - ( [!f1, x1, x2, x3, x4, x5!] + [!f2, x1, x2, x3, x4, x5!])) / (x0 - x5)) by Th12

      .= ((( [!f1, x0, x1, x2, x3, x4!] - [!f1, x1, x2, x3, x4, x5!]) + ( [!f2, x0, x1, x2, x3, x4!] - [!f2, x1, x2, x3, x4, x5!])) / (x0 - x5));

      hence thesis by XCMPLX_1: 62;

    end;

    theorem :: DIFF_2:16

     [!((r1 (#) f1) + (r2 (#) f2)), x0, x1, x2, x3, x4, x5!] = ((r1 * [!f1, x0, x1, x2, x3, x4, x5!]) + (r2 * [!f2, x0, x1, x2, x3, x4, x5!]))

    proof

       [!((r1 (#) f1) + (r2 (#) f2)), x0, x1, x2, x3, x4, x5!] = ( [!(r1 (#) f1), x0, x1, x2, x3, x4, x5!] + [!(r2 (#) f2), x0, x1, x2, x3, x4, x5!]) by Th15

      .= ((r1 * [!f1, x0, x1, x2, x3, x4, x5!]) + [!(r2 (#) f2), x0, x1, x2, x3, x4, x5!]) by Th14;

      hence thesis by Th14;

    end;

    theorem :: DIFF_2:17

    (x0,x1,x2) are_mutually_distinct implies [!f, x0, x1, x2!] = ((((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1))))

    proof

      assume

       A1: (x0,x1,x2) are_mutually_distinct ;

      then

       A2: (x1 - x2) <> 0 by ZFMISC_1:def 5;

      

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

      

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

       [!f, x0, x1, x2!] = (((((f . x0) - (f . x1)) / (x0 - x1)) / (x0 - x2)) - ((((f . x1) - (f . x2)) / (x1 - x2)) / (x0 - x2))) by XCMPLX_1: 120

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

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

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

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

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

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

      .= ((((f . x0) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) * (x1 - x2)) / (((x0 - x1) * (x0 - x2)) * (x1 - x2))) + (((f . x1) * (x0 - x1)) / (((x1 - x2) * (x0 - x2)) * (x0 - x1))))) + ((f . x2) / ((x1 - x2) * (x0 - x2)))) by A3, XCMPLX_1: 91

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

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

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

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

      hence thesis by XCMPLX_1: 189;

    end;

    theorem :: DIFF_2:18

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

    proof

      set x10 = (x1 - x0);

      set x20 = (x2 - x0);

      set x30 = (x3 - x0);

      set x12 = (x1 - x2);

      set x13 = (x1 - x3);

      set x23 = (x2 - x3);

      assume

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

      then

       A2: (x2 - x3) <> 0 by ZFMISC_1:def 6;

      

       A3: (x3 - x0) <> 0 by A1, ZFMISC_1:def 6;

      

       A4: (x1 - x3) <> 0 by A1, ZFMISC_1:def 6;

      

       A5: (x1 - x0) <> 0 by A1, ZFMISC_1:def 6;

      

       A6: (x2 - x0) <> 0 by A1, ZFMISC_1:def 6;

      

       A7: (x1 - x2) <> 0 by A1, ZFMISC_1:def 6;

      

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

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

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

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

      .= ((((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / (x10 * x12)) / x20) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)) by A7, A5, XCMPLX_1: 116

      .= ((((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / (x10 * x12)) / x20) - ((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (x12 * x23)) / x13)) / (x0 - x3)) by A2, A7, XCMPLX_1: 130

      .= (((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20)) - ((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (x12 * x23)) / x13)) / (x0 - x3)) by XCMPLX_1: 78

      .= (((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20)) - (((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13))) / (x0 - x3)) by XCMPLX_1: 78

      .= (( - ((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20)) - (((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13)))) / ( - (x0 - x3))) by XCMPLX_1: 191

      .= (((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13)) - (((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20))) / (x3 - x0))

      .= (((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13)) / x30) - ((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20)) / x30)) by XCMPLX_1: 120

      .= ((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (((x12 * x23) * x13) * x30)) - ((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20)) / x30)) by XCMPLX_1: 78

      .= ((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (((x12 * x23) * x13) * x30)) - (((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / (((x10 * x12) * x20) * x30))) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) * x20) / ((((x12 * x23) * x13) * x30) * x20)) - (((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / (((x10 * x12) * x20) * x30))) by A6, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x23) * x20) - ((((f . x2) - (f . x3)) * x12) * x20)) * x10) / (((((x12 * x20) * x30) * x23) * x13) * x10)) - (((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / (((x10 * x12) * x20) * x30))) by A5, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x23) * x20) * x10) - (((((f . x2) - (f . x3)) * x12) * x20) * x10)) / (((((x12 * x20) * x30) * x23) * x13) * x10)) - ((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) * (x23 * x13)) / ((((x12 * x20) * x30) * x10) * (x23 * x13)))) by A2, A4, XCMPLX_1: 6, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x23) * x20) * x10) - (((((f . x2) - (f . x3)) * x12) * x20) * x10)) - ((((((f . x0) - (f . x1)) * x12) * x23) * x13) + (((((f . x1) - (f . x2)) * x10) * x23) * x13))) / (((((x12 * x20) * x30) * x23) * x13) * x10)) by XCMPLX_1: 120

      .= ((((( - ((((f . x0) * x12) * x23) * x13)) + ((((f . x1) * x20) * x23) * x30)) - ((((f . x2) * x13) * x10) * x30)) + ((((f . x3) * x12) * x20) * x10)) / (((((x12 * x20) * x30) * x23) * x13) * x10));

      

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

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

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

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

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

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

      .= (((((((f . x3) - (f . x2)) / x23) - (((f . x2) - (f . x1)) / x12)) / x13) + ( - (( - ((((f . x1) - (f . x0)) / x10) + (((f . x2) - (f . x1)) / x12))) / x20))) / x30)

      .= (((((((f . x3) - (f . x2)) / x23) - (((f . x2) - (f . x1)) / x12)) / x13) + (((((f . x1) - (f . x0)) / x10) + (((f . x2) - (f . x1)) / x12)) / x20)) / x30) by XCMPLX_1: 190

      .= ((((((((f . x3) - (f . x2)) * x12) - (((f . x2) - (f . x1)) * x23)) / (x23 * x12)) / x13) + (((((f . x1) - (f . x0)) / x10) + (((f . x2) - (f . x1)) / x12)) / x20)) / x30) by A2, A7, XCMPLX_1: 130

      .= ((((((((f . x3) - (f . x2)) * x12) - (((f . x2) - (f . x1)) * x23)) / (x23 * x12)) / x13) + ((((((f . x1) - (f . x0)) * x12) + (((f . x2) - (f . x1)) * x10)) / (x10 * x12)) / x20)) / x30) by A7, A5, XCMPLX_1: 116

      .= (((((((f . x3) - (f . x2)) * x12) - (((f . x2) - (f . x1)) * x23)) / ((x23 * x12) * x13)) + ((((((f . x1) - (f . x0)) * x12) + (((f . x2) - (f . x1)) * x10)) / (x10 * x12)) / x20)) / x30) by XCMPLX_1: 78

      .= (((((((f . x3) - (f . x2)) * x12) - (((f . x2) - (f . x1)) * x23)) / ((x23 * x12) * x13)) + (((((f . x1) - (f . x0)) * x12) + (((f . x2) - (f . x1)) * x10)) / ((x10 * x12) * x20))) / x30) by XCMPLX_1: 78

      .= (((((((f . x3) - (f . x2)) * x12) - (((f . x2) - (f . x1)) * x23)) / ((x23 * x12) * x13)) + ((((((f . x1) - (f . x0)) * x12) + (((f . x2) - (f . x1)) * x10)) * x13) / (((x10 * x12) * x20) * x13))) / x30) by A4, XCMPLX_1: 91

      .= (((((((f . x3) - (f . x2)) * x12) - (((f . x2) - (f . x1)) * x23)) / ((x23 * x12) * x13)) + (((((((f . x1) - (f . x0)) * x12) * x13) + ((((f . x2) - (f . x1)) * x10) * x13)) * x23) / ((((x10 * x12) * x13) * x20) * x23))) / x30) by A2, XCMPLX_1: 91

      .= ((((((((f . x3) - (f . x2)) * x12) - (((f . x2) - (f . x1)) * x23)) * x20) / (((x23 * x12) * x13) * x20)) + (((((((f . x1) - (f . x0)) * x12) * x13) * x23) + (((((f . x2) - (f . x1)) * x10) * x13) * x23)) / ((((x10 * x12) * x13) * x20) * x23))) / x30) by A6, XCMPLX_1: 91

      .= (((((((((f . x3) - (f . x2)) * x12) * x20) - ((((f . x2) - (f . x1)) * x23) * x20)) * x10) / ((((x12 * x13) * x20) * x23) * x10)) + (((((((f . x1) - (f . x0)) * x12) * x13) * x23) + (((((f . x2) - (f . x1)) * x10) * x13) * x23)) / ((((x10 * x12) * x13) * x20) * x23))) / x30) by A5, XCMPLX_1: 91

      .= (((((((((f . x3) - (f . x2)) * x12) * x20) * x10) - (((((f . x2) - (f . x1)) * x23) * x20) * x10)) / ((((x10 * x12) * x13) * x20) * x23)) / x30) + ((((((((f . x1) - (f . x0)) * x12) * x13) * x23) + (((((f . x2) - (f . x1)) * x10) * x13) * x23)) / ((((x10 * x12) * x13) * x20) * x23)) / x30)) by XCMPLX_1: 62

      .= ((((((((f . x3) - (f . x2)) * x12) * x20) * x10) - (((((f . x2) - (f . x1)) * x23) * x20) * x10)) / (((((x10 * x12) * x13) * x20) * x23) * x30)) + ((((((((f . x1) - (f . x0)) * x12) * x13) * x23) + (((((f . x2) - (f . x1)) * x10) * x13) * x23)) / ((((x10 * x12) * x13) * x20) * x23)) / x30)) by XCMPLX_1: 78

      .= ((((((((f . x3) - (f . x2)) * x12) * x20) * x10) - (((((f . x2) - (f . x1)) * x23) * x20) * x10)) / (((((x10 * x12) * x13) * x20) * x23) * x30)) + (((((((f . x1) - (f . x0)) * x12) * x13) * x23) + (((((f . x2) - (f . x1)) * x10) * x13) * x23)) / (((((x10 * x12) * x13) * x20) * x23) * x30))) by XCMPLX_1: 78

      .= ((((((((f . x3) - (f . x2)) * x12) * x20) * x10) - (((((f . x2) - (f . x1)) * x23) * x20) * x10)) + ((((((f . x1) - (f . x0)) * x12) * x13) * x23) + (((((f . x2) - (f . x1)) * x10) * x13) * x23))) / (((((x10 * x12) * x13) * x20) * x23) * x30)) by XCMPLX_1: 62

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

       [!f, x1, x2, x3, x0!] = ((((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (x12 * x23)) / x13) - (((((f . x2) - (f . x3)) / (x2 - x3)) - (((f . x3) - (f . x0)) / (x3 - x0))) / (x2 - x0))) / (x1 - x0)) by A2, A7, XCMPLX_1: 130

      .= ((((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (x12 * x23)) / x13) - ((((((f . x2) - (f . x3)) * x30) - (((f . x3) - (f . x0)) * x23)) / (x23 * x30)) / x20)) / x10) by A2, A3, XCMPLX_1: 130

      .= (((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13)) - ((((((f . x2) - (f . x3)) * x30) - (((f . x3) - (f . x0)) * x23)) / (x23 * x30)) / x20)) / x10) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13)) - (((((f . x2) - (f . x3)) * x30) - (((f . x3) - (f . x0)) * x23)) / ((x23 * x30) * x20))) / x10) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13)) / x10) - ((((((f . x2) - (f . x3)) * x30) - (((f . x3) - (f . x0)) * x23)) / ((x23 * x30) * x20)) / x10)) by XCMPLX_1: 120

      .= ((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (((x12 * x23) * x13) * x10)) - ((((((f . x2) - (f . x3)) * x30) - (((f . x3) - (f . x0)) * x23)) / ((x23 * x30) * x20)) / x10)) by XCMPLX_1: 78

      .= ((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (((x12 * x23) * x13) * x10)) - (((((f . x2) - (f . x3)) * x30) - (((f . x3) - (f . x0)) * x23)) / (((x23 * x30) * x20) * x10))) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) * x30) / ((((x12 * x23) * x13) * x10) * x30)) - (((((f . x2) - (f . x3)) * x30) - (((f . x3) - (f . x0)) * x23)) / (((x23 * x30) * x20) * x10))) by A3, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x23) * x30) - ((((f . x2) - (f . x3)) * x12) * x30)) * x20) / (((((x12 * x23) * x13) * x10) * x30) * x20)) - (((((f . x2) - (f . x3)) * x30) - (((f . x3) - (f . x0)) * x23)) / (((x23 * x30) * x20) * x10))) by A6, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x23) * x30) * x20) - (((((f . x2) - (f . x3)) * x12) * x30) * x20)) / (((((x12 * x23) * x13) * x10) * x30) * x20)) - ((((((f . x2) - (f . x3)) * x30) - (((f . x3) - (f . x0)) * x23)) * x13) / ((((x10 * x30) * x20) * x23) * x13))) by A4, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x23) * x30) * x20) - (((((f . x2) - (f . x3)) * x12) * x30) * x20)) / (((((x12 * x23) * x13) * x10) * x30) * x20)) - (((((((f . x2) - (f . x3)) * x30) * x13) - ((((f . x3) - (f . x0)) * x23) * x13)) * x12) / (((((x23 * x13) * x10) * x30) * x20) * x12))) by A7, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x23) * x30) * x20) - (((((f . x2) - (f . x3)) * x12) * x30) * x20)) - ((((((f . x2) - (f . x3)) * x30) * x13) * x12) - (((((f . x3) - (f . x0)) * x23) * x13) * x12))) / (((((x12 * x23) * x13) * x10) * x30) * x20)) by XCMPLX_1: 120

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

      hence thesis by A9;

    end;

    theorem :: DIFF_2:19

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

    proof

      set x10 = (x1 - x0);

      set x20 = (x2 - x0);

      set x30 = (x3 - x0);

      set x12 = (x1 - x2);

      set x13 = (x1 - x3);

      set x23 = (x2 - x3);

      assume

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

      then

       A2: (x2 - x3) <> 0 by ZFMISC_1:def 6;

      

       A3: (x1 - x3) <> 0 by A1, ZFMISC_1:def 6;

      

       A4: (x1 - x2) <> 0 by A1, ZFMISC_1:def 6;

      

       A5: (x3 - x0) <> 0 by A1, ZFMISC_1:def 6;

      

       A6: (x2 - x0) <> 0 by A1, ZFMISC_1:def 6;

      

       A7: (x1 - x0) <> 0 by A1, ZFMISC_1:def 6;

      

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

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

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

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

      .= ((((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / (x10 * x12)) / x20) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)) by A4, A7, XCMPLX_1: 116

      .= ((((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / (x10 * x12)) / x20) - ((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (x12 * x23)) / x13)) / (x0 - x3)) by A2, A4, XCMPLX_1: 130

      .= (((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20)) - ((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (x12 * x23)) / x13)) / (x0 - x3)) by XCMPLX_1: 78

      .= (((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20)) - (((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13))) / (x0 - x3)) by XCMPLX_1: 78

      .= (( - ((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20)) - (((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13)))) / ( - (x0 - x3))) by XCMPLX_1: 191

      .= (((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13)) - (((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20))) / (x3 - x0))

      .= (((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / ((x12 * x23) * x13)) / x30) - ((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20)) / x30)) by XCMPLX_1: 120

      .= ((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (((x12 * x23) * x13) * x30)) - ((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / ((x10 * x12) * x20)) / x30)) by XCMPLX_1: 78

      .= ((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) / (((x12 * x23) * x13) * x30)) - (((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / (((x10 * x12) * x20) * x30))) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x2)) * x23) - (((f . x2) - (f . x3)) * x12)) * x20) / ((((x12 * x23) * x13) * x30) * x20)) - (((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / (((x10 * x12) * x20) * x30))) by A6, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x23) * x20) - ((((f . x2) - (f . x3)) * x12) * x20)) * x10) / (((((x12 * x20) * x30) * x23) * x13) * x10)) - (((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) / (((x10 * x12) * x20) * x30))) by A7, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x23) * x20) * x10) - (((((f . x2) - (f . x3)) * x12) * x20) * x10)) / (((((x12 * x20) * x30) * x23) * x13) * x10)) - ((((((f . x0) - (f . x1)) * x12) + (((f . x1) - (f . x2)) * x10)) * (x23 * x13)) / ((((x12 * x20) * x30) * x10) * (x23 * x13)))) by A2, A3, XCMPLX_1: 6, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x23) * x20) * x10) - (((((f . x2) - (f . x3)) * x12) * x20) * x10)) - ((((((f . x0) - (f . x1)) * x12) * x23) * x13) + (((((f . x1) - (f . x2)) * x10) * x23) * x13))) / (((((x12 * x20) * x30) * x23) * x13) * x10)) by XCMPLX_1: 120

      .= ((((( - ((((f . x0) * x12) * x23) * x13)) + ((((f . x1) * x20) * x23) * x30)) - ((((f . x2) * x13) * x10) * x30)) + ((((f . x3) * x12) * x20) * x10)) / (((((x12 * x20) * x30) * x23) * x13) * x10));

      

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

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

      .= ((((((((f . x1) - (f . x2)) * x20) - (((f . x2) - (f . x0)) * x12)) / (x12 * x20)) / x10) - (((((f . x2) - (f . x0)) / x20) + (((f . x0) - (f . x3)) / x30)) / x23)) / x13) by A4, A6, XCMPLX_1: 130

      .= ((((((((f . x1) - (f . x2)) * x20) - (((f . x2) - (f . x0)) * x12)) / (x12 * x20)) / x10) - ((((((f . x2) - (f . x0)) * x30) + (((f . x0) - (f . x3)) * x20)) / (x30 * x20)) / x23)) / x13) by A5, A6, XCMPLX_1: 116

      .= (((((((f . x1) - (f . x2)) * x20) - (((f . x2) - (f . x0)) * x12)) / ((x12 * x20) * x10)) - ((((((f . x2) - (f . x0)) * x30) + (((f . x0) - (f . x3)) * x20)) / (x30 * x20)) / x23)) / x13) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x2)) * x20) - (((f . x2) - (f . x0)) * x12)) / ((x12 * x20) * x10)) - (((((f . x2) - (f . x0)) * x30) + (((f . x0) - (f . x3)) * x20)) / ((x30 * x20) * x23))) / x13) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x2)) * x20) - (((f . x2) - (f . x0)) * x12)) / ((x12 * x20) * x10)) / x13) - ((((((f . x2) - (f . x0)) * x30) + (((f . x0) - (f . x3)) * x20)) / ((x30 * x20) * x23)) / x13)) by XCMPLX_1: 120

      .= ((((((f . x1) - (f . x2)) * x20) - (((f . x2) - (f . x0)) * x12)) / (((x12 * x20) * x10) * x13)) - ((((((f . x2) - (f . x0)) * x30) + (((f . x0) - (f . x3)) * x20)) / ((x30 * x20) * x23)) / x13)) by XCMPLX_1: 78

      .= ((((((f . x1) - (f . x2)) * x20) - (((f . x2) - (f . x0)) * x12)) / (((x12 * x20) * x10) * x13)) - (((((f . x2) - (f . x0)) * x30) + (((f . x0) - (f . x3)) * x20)) / (((x30 * x20) * x23) * x13))) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x2)) * x20) - (((f . x2) - (f . x0)) * x12)) * x30) / ((((x12 * x20) * x10) * x13) * x30)) - (((((f . x2) - (f . x0)) * x30) + (((f . x0) - (f . x3)) * x20)) / (((x30 * x20) * x23) * x13))) by A5, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x20) * x30) - ((((f . x2) - (f . x0)) * x12) * x30)) * x23) / (((((x12 * x20) * x10) * x13) * x30) * x23)) - (((((f . x2) - (f . x0)) * x30) + (((f . x0) - (f . x3)) * x20)) / (((x30 * x20) * x23) * x13))) by A2, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x20) * x30) * x23) - (((((f . x2) - (f . x0)) * x12) * x30) * x23)) / (((((x12 * x20) * x10) * x13) * x30) * x23)) - ((((((f . x2) - (f . x0)) * x30) + (((f . x0) - (f . x3)) * x20)) * x12) / ((((x30 * x20) * x23) * x13) * x12))) by A4, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x20) * x30) * x23) - (((((f . x2) - (f . x0)) * x12) * x30) * x23)) / (((((x12 * x20) * x10) * x13) * x30) * x23)) - (((((((f . x2) - (f . x0)) * x30) * x12) + ((((f . x0) - (f . x3)) * x20) * x12)) * x10) / (((((x30 * x20) * x23) * x13) * x12) * x10))) by A7, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x2)) * x20) * x30) * x23) - (((((f . x2) - (f . x0)) * x12) * x30) * x23)) - ((((((f . x2) - (f . x0)) * x30) * x12) * x10) + (((((f . x0) - (f . x3)) * x20) * x12) * x10))) / (((((x30 * x20) * x23) * x13) * x12) * x10)) by XCMPLX_1: 120

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

       [!f, x1, x0, x2, x3!] = (((((((f . x1) - (f . x0)) / (x1 - x0)) - ( - (((f . x0) - (f . x2)) / (x2 - x0)))) / (x1 - x2)) - (((((f . x0) - (f . x2)) / ( - (x2 - x0))) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x0 - x3))) / (x1 - x3)) by XCMPLX_1: 188

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

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

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

      .= ((((((((f . x1) - (f . x0)) * x20) + (((f . x0) - (f . x2)) * x10)) / (x20 * x10)) / x12) - (((((f . x0) - (f . x2)) / x20) + (((f . x2) - (f . x3)) / x23)) / x30)) / x13) by A6, A7, XCMPLX_1: 116

      .= ((((((((f . x1) - (f . x0)) * x20) + (((f . x0) - (f . x2)) * x10)) / (x10 * x20)) / x12) - ((((((f . x0) - (f . x2)) * x23) + (((f . x2) - (f . x3)) * x20)) / (x23 * x20)) / x30)) / x13) by A2, A6, XCMPLX_1: 116

      .= (((((((f . x1) - (f . x0)) * x20) + (((f . x0) - (f . x2)) * x10)) / ((x10 * x20) * x12)) - ((((((f . x0) - (f . x2)) * x23) + (((f . x2) - (f . x3)) * x20)) / (x23 * x20)) / x30)) / x13) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x0)) * x20) + (((f . x0) - (f . x2)) * x10)) / ((x10 * x20) * x12)) - (((((f . x0) - (f . x2)) * x23) + (((f . x2) - (f . x3)) * x20)) / ((x23 * x20) * x30))) / x13) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x0)) * x20) + (((f . x0) - (f . x2)) * x10)) / ((x10 * x20) * x12)) / x13) - ((((((f . x0) - (f . x2)) * x23) + (((f . x2) - (f . x3)) * x20)) / ((x23 * x20) * x30)) / x13)) by XCMPLX_1: 120

      .= ((((((f . x1) - (f . x0)) * x20) + (((f . x0) - (f . x2)) * x10)) / (((x10 * x20) * x12) * x13)) - ((((((f . x0) - (f . x2)) * x23) + (((f . x2) - (f . x3)) * x20)) / ((x23 * x20) * x30)) / x13)) by XCMPLX_1: 78

      .= ((((((f . x1) - (f . x0)) * x20) + (((f . x0) - (f . x2)) * x10)) / (((x10 * x20) * x12) * x13)) - (((((f . x0) - (f . x2)) * x23) + (((f . x2) - (f . x3)) * x20)) / (((x23 * x20) * x30) * x13))) by XCMPLX_1: 78

      .= (((((((f . x1) - (f . x0)) * x20) + (((f . x0) - (f . x2)) * x10)) * x23) / ((((x10 * x20) * x12) * x13) * x23)) - (((((f . x0) - (f . x2)) * x23) + (((f . x2) - (f . x3)) * x20)) / (((x23 * x20) * x30) * x13))) by A2, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x0)) * x20) * x23) + ((((f . x0) - (f . x2)) * x10) * x23)) * x30) / (((((x10 * x20) * x12) * x13) * x23) * x30)) - (((((f . x0) - (f . x2)) * x23) + (((f . x2) - (f . x3)) * x20)) / (((x23 * x20) * x30) * x13))) by A5, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x0)) * x20) * x23) * x30) + (((((f . x0) - (f . x2)) * x10) * x23) * x30)) / (((((x10 * x20) * x12) * x13) * x23) * x30)) - ((((((f . x0) - (f . x2)) * x23) + (((f . x2) - (f . x3)) * x20)) * x10) / ((((x23 * x20) * x30) * x13) * x10))) by A7, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x0)) * x20) * x23) * x30) + (((((f . x0) - (f . x2)) * x10) * x23) * x30)) / (((((x10 * x20) * x12) * x13) * x23) * x30)) - (((((((f . x0) - (f . x2)) * x23) * x10) + ((((f . x2) - (f . x3)) * x20) * x10)) * x12) / (((((x23 * x20) * x30) * x13) * x10) * x12))) by A4, XCMPLX_1: 91

      .= ((((((((f . x1) - (f . x0)) * x20) * x23) * x30) + (((((f . x0) - (f . x2)) * x10) * x23) * x30)) - ((((((f . x0) - (f . x2)) * x23) * x10) * x12) + (((((f . x2) - (f . x3)) * x20) * x10) * x12))) / (((((x23 * x20) * x30) * x13) * x10) * x12)) by XCMPLX_1: 120

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

      hence thesis by A9;

    end;

    theorem :: DIFF_2:20

    f is constant implies [!f, x0, x1, x2!] = 0

    proof

      assume

       A1: f is constant;

      

      then [!f, x0, x1, x2!] = (( 0 qua Nat - [!f, x1, x2!]) / (x0 - x2)) by DIFF_1: 30

      .= (( 0 qua Nat - 0 qua Nat) / (x0 - x2)) by A1, DIFF_1: 30;

      hence thesis;

    end;

    theorem :: DIFF_2:21

    

     Th21: x0 <> x1 implies [!( AffineMap (a,b)), x0, x1!] = a

    proof

      assume x0 <> x1;

      then

       A1: (x0 - x1) <> 0 ;

       [!( AffineMap (a,b)), x0, x1!] = ((((a * x0) + b) - (( AffineMap (a,b)) . x1)) / (x0 - x1)) by FCONT_1:def 4

      .= ((((a * x0) + b) - ((a * x1) + b)) / (x0 - x1)) by FCONT_1:def 4

      .= ((a * (x0 - x1)) / (x0 - x1));

      hence thesis by A1, XCMPLX_1: 89;

    end;

    theorem :: DIFF_2:22

    

     Th22: (x0,x1,x2) are_mutually_distinct implies [!( AffineMap (a,b)), x0, x1, x2!] = 0

    proof

      assume

       A1: (x0,x1,x2) are_mutually_distinct ;

      then

       A2: x1 <> x2 by ZFMISC_1:def 5;

      x0 <> x1 by A1, ZFMISC_1:def 5;

      

      then [!( AffineMap (a,b)), x0, x1, x2!] = ((a - [!( AffineMap (a,b)), x1, x2!]) / (x0 - x2)) by Th21

      .= ((a - a) / (x0 - x2)) by A2, Th21;

      hence thesis;

    end;

    theorem :: DIFF_2:23

    (x0,x1,x2,x3) are_mutually_distinct implies [!( AffineMap (a,b)), x0, x1, x2, x3!] = 0

    proof

      assume

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

      then

       A2: x1 <> x2 by ZFMISC_1:def 6;

      x1 <> x3 & x2 <> x3 by A1, ZFMISC_1:def 6;

      then

       A3: (x1,x2,x3) are_mutually_distinct by A2, ZFMISC_1:def 5;

      x0 <> x1 & x0 <> x2 by A1, ZFMISC_1:def 6;

      then (x0,x1,x2) are_mutually_distinct by A2, ZFMISC_1:def 5;

      

      then [!( AffineMap (a,b)), x0, x1, x2, x3!] = (( 0 qua Nat - [!( AffineMap (a,b)), x1, x2, x3!]) / (x0 - x3)) by Th22

      .= (( 0 qua Nat - 0 qua Nat) / (x0 - x3)) by A3, Th22;

      hence thesis;

    end;

    theorem :: DIFF_2:24

    for x holds (( fD (( AffineMap (a,b)),h)) . x) = (a * h)

    proof

      let x;

      (( fD (( AffineMap (a,b)),h)) . x) = ((( AffineMap (a,b)) . (x + h)) - (( AffineMap (a,b)) . x)) by DIFF_1: 3

      .= (((a * (x + h)) + b) - (( AffineMap (a,b)) . x)) by FCONT_1:def 4

      .= ((((a * x) + (a * h)) + b) - ((a * x) + b)) by FCONT_1:def 4;

      hence thesis;

    end;

    theorem :: DIFF_2:25

    for x holds (( bD (( AffineMap (a,b)),h)) . x) = (a * h)

    proof

      let x;

      (( bD (( AffineMap (a,b)),h)) . x) = ((( AffineMap (a,b)) . x) - (( AffineMap (a,b)) . (x - h))) by DIFF_1: 4

      .= (((a * x) + b) - (( AffineMap (a,b)) . (x - h))) by FCONT_1:def 4

      .= (((a * x) + b) - ((a * (x - h)) + b)) by FCONT_1:def 4;

      hence thesis;

    end;

    theorem :: DIFF_2:26

    for x holds (( cD (( AffineMap (a,b)),h)) . x) = (a * h)

    proof

      let x;

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

      .= (((a * (x + (h / 2))) + b) - (( AffineMap (a,b)) . (x - (h / 2)))) by FCONT_1:def 4

      .= (((a * (x + (h / 2))) + b) - ((a * (x - (h / 2))) + b)) by FCONT_1:def 4;

      hence thesis;

    end;

    theorem :: DIFF_2:27

    

     Th27: (for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c)) & x0 <> x1 implies [!f, x0, x1!] = ((a * (x0 + x1)) + b)

    proof

      assume that

       A1: for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c) and

       A2: x0 <> x1;

      

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

       [!f, x0, x1!] = (((((a * (x0 ^2 )) + (b * x0)) + c) - (f . x1)) / (x0 - x1)) by A1

      .= (((((a * (x0 ^2 )) + (b * x0)) + c) - (((a * (x1 ^2 )) + (b * x1)) + c)) / (x0 - x1)) by A1

      .= ((((a * (x0 + x1)) + b) * (x0 - x1)) / (x0 - x1));

      hence thesis by A3, XCMPLX_1: 89;

    end;

    theorem :: DIFF_2:28

    

     Th28: (for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c)) & (x0,x1,x2) are_mutually_distinct implies [!f, x0, x1, x2!] = a

    proof

      assume

       A1: for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c);

      assume

       A2: (x0,x1,x2) are_mutually_distinct ;

      then

       A3: x1 <> x2 by ZFMISC_1:def 5;

      

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

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

      

      then [!f, x0, x1, x2!] = ((((a * (x0 + x1)) + b) - [!f, x1, x2!]) / (x0 - x2)) by A1, Th27

      .= ((((a * (x0 + x1)) + b) - ((a * (x1 + x2)) + b)) / (x0 - x2)) by A1, A3, Th27

      .= ((a * (x0 - x2)) / (x0 - x2));

      hence thesis by A4, XCMPLX_1: 89;

    end;

    theorem :: DIFF_2:29

    

     Th29: (for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c)) & (x0,x1,x2,x3) are_mutually_distinct implies [!f, x0, x1, x2, x3!] = 0

    proof

      assume

       A1: for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c);

      assume

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

      then

       A3: x1 <> x2 by ZFMISC_1:def 6;

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

      then

       A4: (x1,x2,x3) are_mutually_distinct by A3, ZFMISC_1:def 5;

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

      then (x0,x1,x2) are_mutually_distinct by A3, ZFMISC_1:def 5;

      

      then [!f, x0, x1, x2, x3!] = ((a - [!f, x1, x2, x3!]) / (x0 - x3)) by A1, Th28

      .= ((a - a) / (x0 - x3)) by A1, A4, Th28;

      hence thesis;

    end;

    theorem :: DIFF_2:30

    (for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c)) & (x0,x1,x2,x3,x4) are_mutually_distinct implies [!f, x0, x1, x2, x3, x4!] = 0

    proof

      assume

       A1: for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c);

      assume

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

      then

       A3: x1 <> x2 & x1 <> x3 by ZFMISC_1:def 7;

      

       A4: x0 <> x3 by A2, ZFMISC_1:def 7;

      

       A5: x2 <> x3 by A2, ZFMISC_1:def 7;

      

       A6: x3 <> x4 by A2, ZFMISC_1:def 7;

      x1 <> x4 & x2 <> x4 by A2, ZFMISC_1:def 7;

      then

       A7: (x1,x2,x3,x4) are_mutually_distinct by A3, A5, A6, ZFMISC_1:def 6;

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

      then (x0,x1,x2,x3) are_mutually_distinct by A4, A3, A5, ZFMISC_1:def 6;

      

      then [!f, x0, x1, x2, x3, x4!] = (( 0 qua Nat - [!f, x1, x2, x3, x4!]) / (x0 - x4)) by A1, Th29

      .= (( 0 qua Nat - 0 qua Nat) / (x0 - x4)) by A1, A7, Th29;

      hence thesis;

    end;

    theorem :: DIFF_2:31

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

    proof

      assume

       A1: for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c);

      let x;

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

      .= ((((a * ((x + h) ^2 )) + (b * (x + h))) + c) - (f . x)) by A1

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:32

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

    proof

      assume

       A1: for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c);

      let x;

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

      .= ((((a * (x ^2 )) + (b * x)) + c) - (f . (x - h))) by A1

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

      .= (((((2 * a) * h) * x) - (a * (h ^2 ))) + (b * h));

      hence thesis;

    end;

    theorem :: DIFF_2:33

    (for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c)) implies for x holds (( cD (f,h)) . x) = ((((2 * a) * h) * x) + (b * h))

    proof

      assume

       A1: for x holds (f . x) = (((a * (x ^2 )) + (b * x)) + c);

      let x;

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

      .= ((((a * ((x + (h / 2)) ^2 )) + (b * (x + (h / 2)))) + c) - (f . (x - (h / 2)))) by A1

      .= ((((a * ((x + (h / 2)) ^2 )) + (b * (x + (h / 2)))) + c) - (((a * ((x - (h / 2)) ^2 )) + (b * (x - (h / 2)))) + c)) by A1

      .= ((((2 * a) * h) * x) + (b * h));

      hence thesis;

    end;

    theorem :: DIFF_2:34

    

     Th34: (for x holds (f . x) = (k / x)) & x0 <> x1 & x0 <> 0 & x1 <> 0 implies [!f, x0, x1!] = ( - (k / (x0 * x1)))

    proof

      assume that

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

       A2: x0 <> x1 and

       A3: x0 <> 0 and

       A4: x1 <> 0 ;

      

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

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

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

      .= ((((k * x1) / (x0 * x1)) - (k / x1)) / (x0 - x1)) by A4, XCMPLX_1: 91

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

      .= ((((k * x1) - (k * x0)) / (x0 * x1)) / (x0 - x1)) by XCMPLX_1: 120

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

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

      .= ( - (((k * (x1 - x0)) / (x1 - x0)) / (x0 * x1))) by XCMPLX_1: 48;

      hence thesis by A5, XCMPLX_1: 89;

    end;

    theorem :: DIFF_2:35

    

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

    proof

      assume that

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

       A2: x0 <> 0 and

       A3: x1 <> 0 and

       A4: x2 <> 0 ;

      assume

       A5: (x0,x1,x2) are_mutually_distinct ;

      then

       A6: x1 <> x2 by ZFMISC_1:def 5;

      

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

      x0 <> x1 by A5, ZFMISC_1:def 5;

      

      then [!f, x0, x1, x2!] = ((( - (k / (x0 * x1))) - [!f, x1, x2!]) / (x0 - x2)) by A1, A2, A3, Th34

      .= ((( - (k / (x0 * x1))) - ( - (k / (x1 * x2)))) / (x0 - x2)) by A1, A3, A4, A6, Th34

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

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

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

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

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

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

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

      hence thesis by A7, XCMPLX_1: 91;

    end;

    theorem :: DIFF_2:36

    

     Th36: (for x holds (f . x) = (k / x)) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & (x0,x1,x2,x3) are_mutually_distinct implies [!f, x0, x1, x2, x3!] = ( - (k / (((x0 * x1) * x2) * x3)))

    proof

      assume that

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

       A2: x0 <> 0 and

       A3: x1 <> 0 & x2 <> 0 and

       A4: x3 <> 0 ;

      assume

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

      then

       A6: x1 <> x2 by ZFMISC_1:def 6;

      x1 <> x3 & x2 <> x3 by A5, ZFMISC_1:def 6;

      then

       A7: (x1,x2,x3) are_mutually_distinct by A6, ZFMISC_1:def 5;

      

       A8: (x0 - x3) <> 0 by A5, ZFMISC_1:def 6;

      x0 <> x1 & x0 <> x2 by A5, ZFMISC_1:def 6;

      then (x0,x1,x2) are_mutually_distinct by A6, ZFMISC_1:def 5;

      

      then [!f, x0, x1, x2, x3!] = (((k / ((x0 * x1) * x2)) - [!f, x1, x2, x3!]) / (x0 - x3)) by A1, A2, A3, Th35

      .= (((k / ((x0 * x1) * x2)) - (k / ((x1 * x2) * x3))) / (x0 - x3)) by A1, A3, A4, A7, Th35

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

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

      .= ((((k * x3) - (k * x0)) / (((x0 * x1) * x2) * x3)) / (x0 - x3)) by XCMPLX_1: 120

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

      .= (( - k) / (((x0 * x1) * x2) * x3)) by A8, XCMPLX_1: 91;

      hence thesis by XCMPLX_1: 187;

    end;

    theorem :: DIFF_2:37

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

    proof

      assume that

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

       A2: x0 <> 0 and

       A3: x1 <> 0 & x2 <> 0 & x3 <> 0 and

       A4: x4 <> 0 ;

      assume

       A5: (x0,x1,x2,x3,x4) are_mutually_distinct ;

      then

       A6: x1 <> x2 & x1 <> x3 by ZFMISC_1:def 7;

      

       A7: x3 <> x4 by A5, ZFMISC_1:def 7;

      

       A8: x2 <> x3 by A5, ZFMISC_1:def 7;

      

       A9: (x0 - x4) <> 0 by A5, ZFMISC_1:def 7;

      

       A10: x0 <> x3 by A5, ZFMISC_1:def 7;

      x1 <> x4 & x2 <> x4 by A5, ZFMISC_1:def 7;

      then

       A11: (x1,x2,x3,x4) are_mutually_distinct by A6, A8, A7, ZFMISC_1:def 6;

      x0 <> x1 & x0 <> x2 by A5, ZFMISC_1:def 7;

      then (x0,x1,x2,x3) are_mutually_distinct by A10, A6, A8, ZFMISC_1:def 6;

      

      then [!f, x0, x1, x2, x3, x4!] = ((( - (k / (((x0 * x1) * x2) * x3))) - [!f, x1, x2, x3, x4!]) / (x0 - x4)) by A1, A2, A3, Th36

      .= ((( - (k / (((x0 * x1) * x2) * x3))) - ( - (k / (((x1 * x2) * x3) * x4)))) / (x0 - x4)) by A1, A3, A4, A11, Th36

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

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

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

      .= ((((k * x0) / ((((x0 * x1) * x2) * x3) * x4)) - ((k * x4) / ((((x0 * x1) * x2) * x3) * x4))) / (x0 - x4))

      .= ((((k * x0) - (k * x4)) / ((((x0 * x1) * x2) * x3) * x4)) / (x0 - x4)) by XCMPLX_1: 120

      .= ((k * (x0 - x4)) / (((((x0 * x1) * x2) * x3) * x4) * (x0 - x4))) by XCMPLX_1: 78;

      hence thesis by A9, XCMPLX_1: 91;

    end;

    theorem :: DIFF_2:38

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

    theorem :: DIFF_2:39

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

    theorem :: DIFF_2:40

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

    proof

      assume

       A1: for x holds (f . x) = (k / x) & (x + (h / 2)) <> 0 & (x - (h / 2)) <> 0 ;

      let x;

      

       A2: (x + (h / 2)) <> 0 by A1;

      

       A3: (x - (h / 2)) <> 0 by A1;

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

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

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

      .= (((k * (x - (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) - (k / (x - (h / 2)))) by A3, XCMPLX_1: 91

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

      .= ((((k * x) - (k * (h / 2))) - (k * (x + (h / 2)))) / ((x - (h / 2)) * (x + (h / 2)))) by XCMPLX_1: 120;

      hence thesis;

    end;

    theorem :: DIFF_2:41

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

    proof

       [! sin , x0, x1!] = ((( sin x0) - ( sin x1)) / (x0 - x1))

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

      hence thesis;

    end;

    theorem :: DIFF_2:42

    for x holds (( fD ( sin ,h)) . x) = (2 * (( cos (((2 * x) + h) / 2)) * ( sin (h / 2))))

    proof

      let x;

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:43

    for x holds (( bD ( sin ,h)) . x) = (2 * (( cos (((2 * x) - h) / 2)) * ( sin (h / 2))))

    proof

      let x;

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:44

    for x holds (( cD ( sin ,h)) . x) = (2 * (( cos x) * ( sin (h / 2))))

    proof

      let x;

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:45

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

    proof

       [! cos , x0, x1!] = ((( cos x0) - ( cos x1)) / (x0 - x1))

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

      hence thesis by XCMPLX_1: 187;

    end;

    theorem :: DIFF_2:46

    for x holds (( fD ( cos ,h)) . x) = ( - (2 * (( sin (((2 * x) + h) / 2)) * ( sin (h / 2)))))

    proof

      let x;

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:47

    for x holds (( bD ( cos ,h)) . x) = ( - (2 * (( sin (((2 * x) - h) / 2)) * ( sin (h / 2)))))

    proof

      let x;

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:48

    for x holds (( cD ( cos ,h)) . x) = ( - (2 * (( sin x) * ( sin (h / 2)))))

    proof

      let x;

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:49

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

    proof

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:50

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

    proof

      let x;

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:51

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

    proof

      let x;

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:52

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

    proof

      let x;

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:53

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

    proof

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:54

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

    proof

      let x;

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

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:55

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

    proof

      let x;

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

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:56

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

    proof

      let x;

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

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:57

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

    proof

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:58

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

    proof

      let x;

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

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:59

    for x holds (( bD (( cos (#) cos ),h)) . x) = ((1 / 2) * (( cos (2 * x)) - ( cos (2 * (x - h)))))

    proof

      let x;

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

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:60

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

    proof

      let x;

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

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

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:61

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

    proof

      set y = (3 * x0);

      set z = (3 * x1);

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

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

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

      .= ((((( sin x0) * ( sin x0)) * ( cos x0)) - ((( sin x1) * ( sin 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)))) - ((( sin x1) * ( sin x1)) * ( cos x1))) / (x0 - x1)) by SIN_COS4: 34

      .= ((((1 / 4) * (( 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: 34

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

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

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

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

      hence thesis by XCMPLX_1: 187;

    end;

    theorem :: DIFF_2:62

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

    proof

      let x;

      set y = (3 * x);

      set z = (3 * h);

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

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

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

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

      .= (((( sin (x + h)) * ( sin (x + h))) * ( cos (x + h))) - ((( sin x) * ( sin 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))))) - ((( sin x) * ( sin x)) * ( cos x))) by SIN_COS4: 34

      .= (((1 / 4) * (( 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: 34

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:63

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

    proof

      let x;

      set y = (3 * x);

      set z = (3 * h);

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

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

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

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

      .= (((( sin x) * ( sin x)) * ( cos x)) - ((( sin (x - h)) * ( sin (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)))) - ((( sin (x - h)) * ( sin (x - h))) * ( cos (x - h)))) by SIN_COS4: 34

      .= (((1 / 4) * (( 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: 34

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:64

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

    proof

      let x;

      set y = (3 * x);

      set z = (3 * h);

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

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

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

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

      .= (((( 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 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)))))) - ((( sin (x - (h / 2))) * ( sin (x - (h / 2)))) * ( cos (x - (h / 2))))) by SIN_COS4: 34

      .= (((1 / 4) * (( 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: 34

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:65

     [!(( sin (#) cos ) (#) cos ), x0, x1!] = (((1 / 2) * ((( 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 (#) cos ) (#) cos ), x0, x1!] = ((((( sin (#) cos ) . x0) * ( cos . x0)) - ((( sin (#) cos ) (#) cos ) . x1)) / (x0 - x1)) by VALUED_1: 5

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

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

      .= ((((( sin x0) * ( cos x0)) * ( cos x0)) - ((( sin x1) * ( cos x1)) * ( cos 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) * ( cos x1)) * ( cos x1))) / (x0 - x1)) by SIN_COS4: 35

      .= ((((1 / 4) * (( 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: 35

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

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

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

      .= (((1 / 2) * ((( 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_2:66

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

    proof

      let x;

      set y = (3 * x);

      set z = (3 * h);

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

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

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

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

      .= (((( sin (x + h)) * ( cos (x + h))) * ( cos (x + h))) - ((( sin x) * ( cos x)) * ( cos 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) * ( cos x)) * ( cos x))) by SIN_COS4: 35

      .= (((1 / 4) * (( 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: 35

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:67

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

    proof

      let x;

      set y = (3 * x);

      set z = (3 * h);

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

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

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

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

      .= (((( sin x) * ( cos x)) * ( cos x)) - ((( sin (x - h)) * ( cos (x - h))) * ( cos (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)) * ( cos (x - h))) * ( cos (x - h)))) by SIN_COS4: 35

      .= (((1 / 4) * (( 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: 35

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:68

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

    proof

      let x;

      set y = (3 * x);

      set z = (3 * h);

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

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

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

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

      .= (((( 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 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))) * ( cos (x - (h / 2)))) * ( cos (x - (h / 2))))) by SIN_COS4: 35

      .= (((1 / 4) * (( 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: 35

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

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

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

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

      hence thesis;

    end;

    theorem :: DIFF_2:69

    x0 in ( dom tan ) & x1 in ( dom tan ) implies [! tan , x0, x1!] = (( sin (x0 - x1)) / ((( cos x0) * ( cos x1)) * (x0 - x1)))

    proof

      assume that

       A1: x0 in ( dom tan ) and

       A2: x1 in ( dom tan );

      

       A3: ( tan . x0) = (( sin . x0) * (( cos . x0) " )) by A1, RFUNCT_1:def 1

      .= (( sin . x0) * (1 / ( cos . x0))) by XCMPLX_1: 215

      .= ( tan x0) by XCMPLX_1: 99;

      

       A4: ( tan . x1) = (( sin . x1) * (( cos . x1) " )) by A2, RFUNCT_1:def 1

      .= (( sin . x1) * (1 / ( cos . x1))) by XCMPLX_1: 215

      .= ( tan x1) by XCMPLX_1: 99;

      ( cos x0) <> 0 & ( cos x1) <> 0 by A1, A2, FDIFF_8: 1;

      

      then [! tan , x0, x1!] = ((( sin (x0 - x1)) / (( cos x0) * ( cos x1))) / (x0 - x1)) by A3, A4, SIN_COS4: 20

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

      hence thesis;

    end;

    theorem :: DIFF_2:70

    x0 in ( dom cot ) & x1 in ( dom cot ) implies [! cot , x0, x1!] = ( - (( sin (x0 - x1)) / ((( sin x0) * ( sin x1)) * (x0 - x1))))

    proof

      assume that

       A1: x0 in ( dom cot ) and

       A2: x1 in ( dom cot );

      

       A3: ( cot . x0) = (( cos . x0) * (( sin . x0) " )) by A1, RFUNCT_1:def 1

      .= (( cos . x0) * (1 / ( sin . x0))) by XCMPLX_1: 215

      .= ( cot x0) by XCMPLX_1: 99;

      

       A4: ( cot . x1) = (( cos . x1) * (( sin . x1) " )) by A2, RFUNCT_1:def 1

      .= (( cos . x1) * (1 / ( sin . x1))) by XCMPLX_1: 215

      .= ( cot x1) by XCMPLX_1: 99;

      ( sin x0) <> 0 & ( sin x1) <> 0 by A1, A2, FDIFF_8: 2;

      

      then [! cot , x0, x1!] = (( - (( sin (x0 - x1)) / (( sin x0) * ( sin x1)))) / (x0 - x1)) by A3, A4, SIN_COS4: 24

      .= ( - ((( sin (x0 - x1)) / (( sin x0) * ( sin x1))) / (x0 - x1))) by XCMPLX_1: 187;

      hence thesis by XCMPLX_1: 78;

    end;

    theorem :: DIFF_2:71

    x0 in ( dom cosec ) & x1 in ( dom cosec ) implies [! cosec , x0, x1!] = (((2 * ( cos ((x1 + x0) / 2))) * ( sin ((x1 - x0) / 2))) / ((( sin x1) * ( sin x0)) * (x0 - x1)))

    proof

      assume that

       A1: x0 in ( dom cosec ) and

       A2: x1 in ( dom cosec );

      

       A3: ( cosec . x1) = (( sin . x1) " ) by A2, RFUNCT_1:def 2

      .= ( cosec x1) by XCMPLX_1: 215;

      ( cosec . x0) = (( sin . x0) " ) by A1, RFUNCT_1:def 2

      .= ( cosec x0) by XCMPLX_1: 215;

      

      then [! cosec , x0, x1!] = ((((1 * ( sin x1)) / (( sin x0) * ( sin x1))) - (1 / ( sin x1))) / (x0 - x1)) by A2, A3, RFUNCT_1: 3, XCMPLX_1: 91

      .= ((((1 * ( sin x1)) / (( sin x0) * ( sin x1))) - ((1 * ( sin x0)) / (( sin x1) * ( sin x0)))) / (x0 - x1)) by A1, RFUNCT_1: 3, XCMPLX_1: 91

      .= (((( sin x1) - ( sin x0)) / (( sin x1) * ( sin x0))) / (x0 - x1)) by XCMPLX_1: 120

      .= ((( sin x1) - ( sin x0)) / ((( sin x1) * ( sin x0)) * (x0 - x1))) by XCMPLX_1: 78

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

      hence thesis;

    end;

    theorem :: DIFF_2:72

    x0 in ( dom sec ) & x1 in ( dom sec ) implies [! sec , x0, x1!] = ( - (((2 * ( sin ((x1 + x0) / 2))) * ( sin ((x1 - x0) / 2))) / ((( cos x1) * ( cos x0)) * (x0 - x1))))

    proof

      assume that

       A1: x0 in ( dom sec ) and

       A2: x1 in ( dom sec );

      

       A3: ( sec . x1) = (( cos . x1) " ) by A2, RFUNCT_1:def 2

      .= ( sec x1) by XCMPLX_1: 215;

      ( sec . x0) = (( cos . x0) " ) by A1, RFUNCT_1:def 2

      .= ( sec x0) by XCMPLX_1: 215;

      

      then [! sec , x0, x1!] = ((((1 * ( cos x1)) / (( cos x0) * ( cos x1))) - (1 / ( cos x1))) / (x0 - x1)) by A2, A3, RFUNCT_1: 3, XCMPLX_1: 91

      .= ((((1 * ( cos x1)) / (( cos x0) * ( cos x1))) - ((1 * ( cos x0)) / (( cos x1) * ( cos x0)))) / (x0 - x1)) by A1, RFUNCT_1: 3, XCMPLX_1: 91

      .= (((( cos x1) - ( cos x0)) / (( cos x1) * ( cos x0))) / (x0 - x1)) by XCMPLX_1: 120

      .= ((( cos x1) - ( cos x0)) / ((( cos x1) * ( cos x0)) * (x0 - x1))) by XCMPLX_1: 78

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

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

      hence thesis;

    end;