polydiff.miz

    begin

    reserve c for Complex;

    reserve r for Real;

    reserve m,n for Nat;

    reserve f for complex-valued Function;

    theorem :: POLYDIFF:1



     Th1: ( 0 + f) = f

    proof

      thus ( dom ( 0 + f)) = ( dom f) by VALUED_1:def 2;

      let x be object;

      assume x in ( dom ( 0 + f));



      hence (( 0 + f) . x) = ( 0 + (f . x)) by VALUED_1:def 2

      .= (f . x);

    end;

    theorem :: POLYDIFF:2

    (f - 0 ) = f

    proof

      thus ( dom (f - 0 )) = ( dom f) by VALUED_1: 3;

      let x be object;

      assume

       A1: x in ( dom (f - 0 ));

      ( dom (f - 0 )) = ( dom f) by VALUED_1: 3;



      hence ((f - 0 ) . x) = ((f . x) - 0 ) by A1, VALUED_1: 3

      .= (f . x);

    end;

    registration

      let f be complex-valued Function;

      reduce ( 0 + f) to f;

      reducibility by Th1;

      reduce (f - 0 ) to f;

      reducibility ;

    end

    theorem :: POLYDIFF:3



     Th3: (c + f) = ((( dom f) --> c) + f)

    proof

      set g = (( dom f) --> c);



       A2: ( dom (c + f)) = ( dom f) by VALUED_1:def 2;



      thus

       A3: ( dom (c + f)) = (( dom g) /\ ( dom f)) by VALUED_1:def 2

      .= ( dom (g + f)) by VALUED_1:def 1;

      let x be object;

      assume

       A4: x in ( dom (c + f));

      then

       A5: (g . x) = c by A2, FUNCOP_1: 7;



      thus ((c + f) . x) = (c + (f . x)) by A4, VALUED_1:def 2

      .= ((g + f) . x) by A3, A4, A5, VALUED_1:def 1;

    end;

    theorem :: POLYDIFF:4



     Th4: (f - c) = (f - (( dom f) --> c))

    proof

      set g = (( dom f) --> c);



       A2: ( dom (f - c)) = ( dom f) by VALUED_1: 3;



      thus

       A3: ( dom (f - c)) = (( dom g) /\ ( dom f)) by VALUED_1: 3

      .= ( dom (f - g)) by VALUED_1: 12;

      let x be object;

      assume

       A4: x in ( dom (f - c));

      then

       A5: (g . x) = c by A2, FUNCOP_1: 7;



      thus ((f - c) . x) = ((f . x) - c) by A3, A4, VALUED_1: 3

      .= ((f - g) . x) by A3, A4, A5, VALUED_1: 13;

    end;

    theorem :: POLYDIFF:5



     Th5: (c (#) f) = ((( dom f) --> c) (#) f)

    proof

      set g = (( dom f) --> c);



       A2: ( dom (c (#) f)) = ( dom f) by VALUED_1:def 5;



      thus

       A3: ( dom (c (#) f)) = (( dom g) /\ ( dom f)) by VALUED_1:def 5

      .= ( dom (g (#) f)) by VALUED_1:def 4;

      let x be object;

      assume

       A4: x in ( dom (c (#) f));

      then

       A5: (g . x) = c by A2, FUNCOP_1: 7;



      thus ((c (#) f) . x) = (c * (f . x)) by VALUED_1: 6

      .= ((g (#) f) . x) by A3, A4, A5, VALUED_1:def 4;

    end;

    theorem :: POLYDIFF:6



     Th6: (f + (( dom f) --> 0 )) = f

    proof



      thus (f + (( dom f) --> 0 )) = (f + 0 ) by Th3

      .= f;

    end;

    theorem :: POLYDIFF:7



     Th7: (f - (( dom f) --> 0 )) = f

    proof



      thus (f - (( dom f) --> 0 )) = (f - 0 ) by Th4

      .= f;

    end;

    theorem :: POLYDIFF:8

    ( #Z 0 ) = ( REAL --> 1)

    proof

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

      ( #Z 0 ) = ( REAL --> s)

      proof

        let r be Element of REAL ;



        thus (( #Z 0 ) . r) = (r #Z 0 ) by TAYLOR_1:def 1

        .= s by PREPOWER: 34

        .= (( REAL --> s) . r);

      end;

      hence thesis;

    end;

    begin

    registration

      cluster differentiable -> continuous for Function of REAL , REAL ;

      coherence

      proof

        let f be Function of REAL , REAL ;

        assume f is differentiable;

        then f is_differentiable_on REAL by FUNCT_2:def 1;

        hence thesis by FDIFF_1: 25;

      end;

    end

    definition

      let f be differentiable Function of REAL , REAL ;

      :: POLYDIFF:def1

      func f `| -> Function of REAL , REAL equals (f `| REAL );

      coherence

      proof

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

        then f is_differentiable_on REAL by FDIFF_1:def 8;

        then ( dom (f `| REAL )) = REAL by FDIFF_1:def 7;

        hence thesis by FUNCT_2: 67;

      end;

    end

    theorem :: POLYDIFF:9



     Th9: for f be Function of REAL , REAL holds f is differentiable iff for r holds f is_differentiable_in r

    proof

      let f be Function of REAL , REAL ;



       A1: (f | REAL ) = f;

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

      hence f is differentiable implies for r holds f is_differentiable_in r by A1, FDIFF_1:def 6, XREAL_0:def 1;

      assume for r holds f is_differentiable_in r;

      hence f is_differentiable_on ( dom f);

    end;

    theorem :: POLYDIFF:10



     Th10: for f be differentiable Function of REAL , REAL holds ((f `| ) . r) = ( diff (f,r))

    proof

      let f be differentiable Function of REAL , REAL ;

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

      then

       A1: f is_differentiable_on REAL by FDIFF_1:def 8;

      r in REAL by XREAL_0:def 1;

      hence thesis by A1, FDIFF_1:def 7;

    end;

    definition

      let f be Function of REAL , REAL ;

      :: original: differentiable

      redefine

      :: POLYDIFF:def2

      attr f is differentiable means for r holds f is_differentiable_in r;

      compatibility by Th9;

    end



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

    registration

      cluster constant -> differentiable for Function of REAL , REAL ;

      coherence

      proof

        let f be Function of REAL , REAL such that

         A1: f is constant;



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

        ex r be Element of REAL st ( rng f) = {r} by A1, FUNCT_2: 111;

        hence thesis by A2, Lm1, FDIFF_1: 11;

      end;

    end

    theorem :: POLYDIFF:11



     Th11: for f be constant Function of REAL , REAL holds (f `| ) = ( REAL --> 0 )

    proof

      let f be constant Function of REAL , REAL ;

      reconsider z = 0 as Element of REAL by XREAL_0:def 1;

      (f `| ) = ( REAL --> z)

      proof

        let r be Element of REAL ;



         A1: (f | REAL ) = f;

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



        hence ((f `| ) . r) = z by A1, Lm1, FDIFF_1: 22

        .= (( REAL --> z) . r);

      end;

      hence thesis;

    end;

    registration

      cluster ( id REAL ) -> differentiable;

      coherence

      proof

        let f be Function of REAL , REAL ;

        assume f = ( id REAL );

        then f is_differentiable_on REAL by Lm1, FDIFF_1: 17;

        hence thesis by FUNCT_2:def 1;

      end;

    end

    theorem :: POLYDIFF:12

    (( id REAL ) `| ) = ( REAL --> 1)

    proof

      set f = ( id REAL );

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

      (f `| ) = ( REAL --> z)

      proof

        let r be Element of REAL ;

        (f | REAL ) = f;



        hence ((f `| ) . r) = z by Lm1, FDIFF_1: 17

        .= (( REAL --> z) . r);

      end;

      hence thesis;

    end;

    registration

      let n;

      cluster ( #Z n) -> differentiable;

      coherence

      proof

        n in NAT by ORDINAL1:def 12;

        then ( #Z n) is_differentiable_on REAL by HFDIFF_1: 8;

        hence thesis by FUNCT_2:def 1;

      end;

    end

    theorem :: POLYDIFF:13



     Th13: (( #Z n) `| ) = (n (#) ( #Z (n - 1)))

    proof

      n in NAT by ORDINAL1:def 12;



      hence (( #Z n) `| ) = ((n (#) ( #Z (n - 1))) | ( [#] REAL )) by HFDIFF_1: 28

      .= (n (#) ( #Z (n - 1)));

    end;

    reserve f,g for differentiable Function of REAL , REAL ;

    registration

      let f, g;

      cluster (f + g) -> differentiable;

      coherence

      proof

        let h be Function of REAL , REAL such that

         A1: h = (f + g);

        let r;

        f is_differentiable_in r & g is_differentiable_in r by Th9;

        hence thesis by A1, FDIFF_1: 13;

      end;

      cluster (f - g) -> differentiable;

      coherence

      proof

        let h be Function of REAL , REAL such that

         A2: h = (f - g);

        let r;

        f is_differentiable_in r & g is_differentiable_in r by Th9;

        hence thesis by A2, FDIFF_1: 14;

      end;

      cluster (f (#) g) -> differentiable;

      coherence

      proof

        let h be Function of REAL , REAL such that

         A3: h = (f (#) g);

        let r;

        f is_differentiable_in r & g is_differentiable_in r by Th9;

        hence thesis by A3, FDIFF_1: 16;

      end;

    end

    registration

      let f, r;

      cluster (r + f) -> differentiable;

      coherence

      proof

        let h be Function of REAL , REAL ;

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

        reconsider g = ( REAL --> r) as differentiable Function of REAL , REAL ;

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

        then (g + f) = (r + f) by Th3;

        hence thesis;

      end;

      cluster (r (#) f) -> differentiable;

      coherence

      proof

        let h be Function of REAL , REAL ;

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

        reconsider g = ( REAL --> r) as differentiable Function of REAL , REAL ;

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

        then (g (#) f) = (r (#) f) by Th5;

        hence thesis;

      end;

      cluster (f - r) -> differentiable;

      coherence ;

    end

    registration

      let f;

      cluster ( - f) -> differentiable;

      coherence ;

      cluster (f ^2 ) -> differentiable;

      coherence ;

    end

    theorem :: POLYDIFF:14



     Th14: ((f + g) `| ) = ((f `| ) + (g `| ))

    proof

      let s be Element of REAL ;



       A1: f is_differentiable_in s & g is_differentiable_in s by Th9;



       A2: ((f `| ) . s) = ( diff (f,s)) & ((g `| ) . s) = ( diff (g,s)) by Th10;



      thus (((f + g) `| ) . s) = ( diff ((f + g),s)) by Th10

      .= (( diff (f,s)) + ( diff (g,s))) by A1, FDIFF_1: 13

      .= (((f `| ) + (g `| )) . s) by A2, VALUED_1: 1;

    end;

    theorem :: POLYDIFF:15



     Th15: ((f - g) `| ) = ((f `| ) - (g `| ))

    proof

      let s be Element of REAL ;



       A1: f is_differentiable_in s & g is_differentiable_in s by Th9;



       A2: ((f `| ) . s) = ( diff (f,s)) & ((g `| ) . s) = ( diff (g,s)) by Th10;



      thus (((f - g) `| ) . s) = ( diff ((f - g),s)) by Th10

      .= (( diff (f,s)) - ( diff (g,s))) by A1, FDIFF_1: 14

      .= (((f `| ) - (g `| )) . s) by A2, VALUED_1: 15;

    end;

    theorem :: POLYDIFF:16

    ((f (#) g) `| ) = ((g (#) (f `| )) + (f (#) (g `| )))

    proof

      let s be Element of REAL ;



       A1: f is_differentiable_in s & g is_differentiable_in s by Th9;



       A2: ((f `| ) . s) = ( diff (f,s)) & ((g `| ) . s) = ( diff (g,s)) by Th10;



       A3: ((g . s) * ((f `| ) . s)) = ((g (#) (f `| )) . s) & ((f . s) * ((g `| ) . s)) = ((f (#) (g `| )) . s) by VALUED_1: 5;



      thus (((f (#) g) `| ) . s) = ( diff ((f (#) g),s)) by Th10

      .= (((g . s) * ( diff (f,s))) + ((f . s) * ( diff (g,s)))) by A1, FDIFF_1: 16

      .= (((g (#) (f `| )) + (f (#) (g `| ))) . s) by A2, A3, VALUED_1: 1;

    end;

    theorem :: POLYDIFF:17

    ((r + f) `| ) = (f `| )

    proof

      reconsider s = r as Element of REAL by XREAL_0:def 1;

      set g = ( REAL --> s);



       A1: (g `| ) = ( REAL --> 0 ) by Th11;



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

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

      then (r + f) = (g + f) by Th3;



      hence ((r + f) `| ) = ((g `| ) + (f `| )) by Th14

      .= (f `| ) by A1, A2, Th6;

    end;

    theorem :: POLYDIFF:18

    ((f - r) `| ) = (f `| )

    proof

      reconsider s = r as Element of REAL by XREAL_0:def 1;

      set g = ( REAL --> s);



       A1: (g `| ) = ( REAL --> 0 ) by Th11;



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

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

      then (f - r) = (f - g) by Th4;



      hence ((f - r) `| ) = ((f `| ) - (g `| )) by Th15

      .= (f `| ) by A1, A2, Th7;

    end;

    theorem :: POLYDIFF:19



     Th19: ((r (#) f) `| ) = (r (#) (f `| ))

    proof

      let s be Element of REAL ;



       A1: f is_differentiable_in s by Th9;



       A2: ((f `| ) . s) = ( diff (f,s)) by Th10;



      thus (((r (#) f) `| ) . s) = ( diff ((r (#) f),s)) by Th10

      .= (r * ( diff (f,s))) by A1, FDIFF_1: 15

      .= ((r (#) (f `| )) . s) by A2, VALUED_1: 6;

    end;

    theorem :: POLYDIFF:20

    (( - f) `| ) = ( - (f `| )) by Th19;

    begin

    reserve L for non empty ZeroStr;

    reserve x for Element of L;

    theorem :: POLYDIFF:21



     Th21: for f be the carrier of L -valued Function holds for a be object holds ( Support (f +* (a,x))) c= (( Support f) \/ {a})

    proof

      let f be the carrier of L -valued Function;

      let a,z be object;

      set g = (f +* (a,x));

      assume

       A1: z in ( Support g);

      a = z or z in ( Support f)

      proof

        assume a <> z;

        then

         A2: (g . z) = (f . z) by FUNCT_7: 32;

        ( dom g) = ( dom f) by FUNCT_7: 30;

        then z in ( dom f) & (g . z) <> ( 0. L) by A1, POLYNOM1:def 3;

        hence thesis by A2, POLYNOM1:def 3;

      end;

      hence thesis by ZFMISC_1: 136;

    end;

    registration

      let L, x;

      let f be finite-Support sequence of L;

      let a be object;

      cluster (f +* (a,x)) -> finite-Support;

      coherence

      proof

        let g be sequence of L such that

         A1: g = (f +* (a,x));



         A2: f is finite-Support;

        ( Support g) c= (( Support f) \/ {a}) by A1, Th21;

        hence thesis by A2;

      end;

    end

    theorem :: POLYDIFF:22



     Th22: for p be Polynomial of L st p <> ( 0_. L) holds (( len p) -' 1) = (( len p) - 1)

    proof

      let p be Polynomial of L;

      assume p <> ( 0_. L);

      then 0 <> ( len p) by POLYNOM4: 5;

      then ( 0 + 1) <= ( len p) by NAT_1: 13;

      hence thesis by XREAL_1: 233;

    end;

    registration

      let L be non empty ZeroStr;

      let x be Element of L;

      cluster <%x%> -> constant;

      coherence

      proof

        ( deg <%x%>) <= (1 - 1) by XREAL_1: 9, ALGSEQ_1:def 5;

        hence ( deg <%x%>) <= 0 ;

      end;

      cluster <%x, ( 0. L)%> -> constant;

      coherence

      proof

         <%x, ( 0. L)%> = <%x%> by POLYNOM5: 43;

        hence thesis;

      end;

    end

    theorem :: POLYDIFF:23



     Th23: for L be non empty ZeroStr holds for p be constant Polynomial of L holds p = ( 0_. L) or p = <%(p . 0 )%>

    proof

      let L be non empty ZeroStr;

      let p be constant Polynomial of L;

      ( deg p) <= 0 by RATFUNC1:def 2;

      then ((( len p) - 1) + 1) <= ( 0 + 1) by XREAL_1: 6;

      hence thesis by ALGSEQ_1:def 5;

    end;

    definition

      let L, x, n;

      :: POLYDIFF:def3

      func seq (n,x) -> sequence of L equals (( 0_. L) +* (n,x));

      coherence ;

    end

    registration

      let L, x, n;

      cluster ( seq (n,x)) -> finite-Support;

      coherence ;

    end

    theorem :: POLYDIFF:24



     Th24: (( seq (n,x)) . n) = x

    proof

      ( dom ( 0_. L)) = NAT ;

      hence thesis by ORDINAL1:def 12, FUNCT_7: 31;

    end;

    theorem :: POLYDIFF:25



     Th25: m <> n implies (( seq (n,x)) . m) = ( 0. L)

    proof

      assume m <> n;



      hence (( seq (n,x)) . m) = (( 0_. L) . m) by FUNCT_7: 32

      .= ( 0. L) by ORDINAL1:def 12, FUNCOP_1: 7;

    end;

    theorem :: POLYDIFF:26



     Th26: (n + 1) is_at_least_length_of ( seq (n,x))

    proof

      let i be Nat such that

       A1: i >= (n + 1);

      (n + 0 ) < (n + 1) by XREAL_1: 8;



      hence (( seq (n,x)) . i) = (( 0_. L) . i) by A1, FUNCT_7: 32

      .= ( 0. L) by ORDINAL1:def 12, FUNCOP_1: 7;

    end;

    theorem :: POLYDIFF:27



     Th27: x <> ( 0. L) implies ( len ( seq (n,x))) = (n + 1)

    proof

      assume

       A1: x <> ( 0. L);

      set p = ( seq (n,x));

      for m st m is_at_least_length_of p holds (n + 1) <= m

      proof

        let m such that

         A2: m is_at_least_length_of p;

        (p . n) = x by Th24;

        hence (n + 1) <= m by A1, A2, NAT_1: 13;

      end;

      hence thesis by Th26, ALGSEQ_1:def 3;

    end;

    theorem :: POLYDIFF:28



     Th28: ( seq (n,( 0. L))) = ( 0_. L)

    proof

      let m be Element of NAT ;

      per cases ;

        suppose m = n;



        hence (( seq (n,( 0. L))) . m) = ( 0. L) by Th24

        .= (( 0_. L) . m);

      end;

        suppose m <> n;

        hence (( seq (n,( 0. L))) . m) = (( 0_. L) . m) by FUNCT_7: 32;

      end;

    end;

    theorem :: POLYDIFF:29



     Th29: for L be right_zeroed non empty addLoopStr, x,y be Element of L holds (( seq (n,x)) + ( seq (n,y))) = ( seq (n,(x + y)))

    proof

      let L be right_zeroed non empty addLoopStr, x,y be Element of L;

      let a be Element of NAT ;



       A1: ((( seq (n,x)) + ( seq (n,y))) . a) = ((( seq (n,x)) . a) + (( seq (n,y)) . a)) by NORMSP_1:def 2;

      per cases ;

        suppose a = n;

        then (( seq (n,x)) . a) = x & (( seq (n,y)) . a) = y & (( seq (n,(x + y))) . a) = (x + y) by Th24;

        hence thesis by NORMSP_1:def 2;

      end;

        suppose a <> n;

        then (( seq (n,x)) . a) = ( 0. L) & (( seq (n,y)) . a) = ( 0. L) & (( seq (n,(x + y))) . a) = ( 0. L) by Th25;

        hence thesis by A1, RLVECT_1:def 4;

      end;

    end;

    theorem :: POLYDIFF:30



     Th30: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for x be Element of L holds ( - ( seq (n,x))) = ( seq (n,( - x)))

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let x be Element of L;

      let a be Element of NAT ;

      ( dom ( - ( seq (n,x)))) = NAT by FUNCT_2:def 1;

      then

       A1: (( - ( seq (n,x))) /. a) = ( - (( seq (n,x)) /. a)) by VFUNCT_1:def 5;

      per cases ;

        suppose a = n;

        then (( seq (n,x)) . a) = x & (( seq (n,( - x))) . a) = ( - x) by Th24;

        hence thesis by A1;

      end;

        suppose a <> n;

        then (( seq (n,x)) . a) = ( 0. L) & (( seq (n,( - x))) . a) = ( 0. L) by Th25;

        hence thesis by A1;

      end;

    end;

    theorem :: POLYDIFF:31

    for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for x,y be Element of L holds (( seq (n,x)) - ( seq (n,y))) = ( seq (n,(x - y)))

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let x,y be Element of L;



      thus (( seq (n,x)) - ( seq (n,y))) = (( seq (n,x)) + ( seq (n,( - y)))) by Th30

      .= ( seq (n,(x - y))) by Th29;

    end;

    definition

      let L be non empty ZeroStr;

      let p be sequence of L;

      let n;

      :: POLYDIFF:def4

      func p || n -> sequence of L equals (p +* (n,( 0. L)));

      coherence ;

    end

    registration

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      let n;

      cluster (p || n) -> finite-Support;

      coherence ;

    end

    theorem :: POLYDIFF:32



     Th32: for L be non empty ZeroStr, p be sequence of L holds ((p || n) . n) = ( 0. L)

    proof

      let L be non empty ZeroStr;

      let p be sequence of L;

      ( dom p) = NAT by FUNCT_2:def 1;

      hence thesis by FUNCT_7: 31, ORDINAL1:def 12;

    end;

    theorem :: POLYDIFF:33

    for L be non empty ZeroStr, p be sequence of L holds m <> n implies ((p || n) . m) = (p . m) by FUNCT_7: 32;

    theorem :: POLYDIFF:34



     Th34: for L be non empty ZeroStr holds (( 0_. L) || n) = ( 0_. L)

    proof

      let L be non empty ZeroStr;

      let m be Element of NAT ;

      m = n or m <> n;

      hence thesis by Th32, FUNCT_7: 32;

    end;

    registration

      let L be non empty ZeroStr;

      let n;

      reduce (( 0_. L) || n) to ( 0_. L);

      reducibility by Th34;

    end

    theorem :: POLYDIFF:35

    for L be non empty ZeroStr, p be Polynomial of L holds n > (( len p) -' 1) implies (p || n) = p

    proof

      let L be non empty ZeroStr, p be Polynomial of L such that

       A1: n > (( len p) -' 1);

      let m be Element of NAT ;

      per cases ;

        suppose p = ( 0_. L);

        hence thesis;

      end;

        suppose that

         A2: m = n and

         A3: p <> ( 0_. L);

         0 <> ( len p) by A3, POLYNOM4: 5;

        then ( 0 - 1) < (( len p) - 1) by XREAL_1: 14;

        then (( - 1) + 1) <= (( len p) - 1) by INT_1: 7;

        then ((( len p) -' 1) + 1) = ( len p) by NAT_D: 72;

        then n >= ( len p) by A1, NAT_1: 13;



        hence (p . m) = ( 0. L) by A2, ALGSEQ_1: 8

        .= ((p || n) . m) by A2, Th32;

      end;

        suppose m <> n;

        hence ((p || n) . m) = (p . m) by FUNCT_7: 32;

      end;

    end;

    theorem :: POLYDIFF:36



     Th36: for L be non empty ZeroStr, p be Polynomial of L holds p <> ( 0_. L) implies ( len (p || (( len p) -' 1))) < ( len p)

    proof

      let L be non empty ZeroStr, p be Polynomial of L;

      assume

       A1: p <> ( 0_. L);

      set m = (( len p) -' 1);



       A2: m = (( len p) - 1) by A1, Th22;



       A3: (( len p) - 1) < (( len p) - 0 ) by XREAL_1: 15;

      ( len p) is_at_least_length_of (p || m)

      proof

        let i be Nat such that

         A4: i >= ( len p);



        thus ((p || m) . i) = (p . i) by A2, A3, A4, FUNCT_7: 32

        .= ( 0. L) by A4, ALGSEQ_1: 8;

      end;

      then

       A5: ( len (p || m)) <= ( len p) by ALGSEQ_1:def 3;

      now

        assume ( len (p || m)) = ( len p);

        then

         A6: ( len (p || m)) is_at_least_length_of p by ALGSEQ_1:def 3;

        m is_at_least_length_of (p || m)

        proof

          let i be Nat;

          assume

           A7: i >= m;

          per cases ;

            suppose

             A8: i <> m;

            then i > m by A7, XXREAL_0: 1;

            then i >= ((( len p) - 1) + 1) by A2, NAT_1: 13;



            hence ( 0. L) = (p . i) by ALGSEQ_1: 8

            .= ((p || m) . i) by A8, FUNCT_7: 32;

          end;

            suppose i = m;

            hence ((p || m) . i) = ( 0. L) by Th32;

          end;

        end;

        then m >= ( len (p || m)) by ALGSEQ_1:def 3;

        then

         A9: (p . m) = ( 0. L) by A6;

        ( len p) <> 0 by A1, POLYNOM4: 5;

        hence contradiction by A9, UPROOTS: 18;

      end;

      hence thesis by A5, XXREAL_0: 1;

    end;

    theorem :: POLYDIFF:37



     Th37: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p be Polynomial of L holds ((p || (( len p) -' 1)) + ( Leading-Monomial p)) = p

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p be Polynomial of L;

      set l = ( Leading-Monomial p);

      set m = (( len p) -' 1);

      let n be Element of NAT ;



       A1: (((p || m) + l) . n) = (((p || m) . n) + (l . n)) by NORMSP_1:def 2;

      per cases ;

        suppose

         A2: n = m;

        ((p || m) . m) = ( 0. L) by Th32;

        hence thesis by A1, A2, POLYNOM4:def 1;

      end;

        suppose

         A3: n <> m;

        then (l . n) = ( 0. L) by POLYNOM4:def 1;

        hence thesis by A1, A3, FUNCT_7: 32;

      end;

    end;

    registration

      let L be non empty ZeroStr;

      let p be constant Polynomial of L;

      cluster ( Leading-Monomial p) -> constant;

      coherence

      proof

        ( deg ( Leading-Monomial p)) = ( deg p) by POLYNOM4: 15;

        hence ( deg ( Leading-Monomial p)) <= 0 by RATFUNC1:def 2;

      end;

    end

    theorem :: POLYDIFF:38



     Th38: for L be add-associative right_zeroed right_complementable distributive unital non empty doubleLoopStr holds for x,y be Element of L holds ( eval (( seq (n,x)),y)) = ((( seq (n,x)) . n) * ( power (y,n)))

    proof

      let L be add-associative right_zeroed right_complementable distributive unital non empty doubleLoopStr;

      let x,y be Element of L;

      set p = ( seq (n,x));

      consider F be FinSequence of L such that

       A1: ( eval (p,y)) = ( Sum F) and

       A2: ( len F) = ( len p) and

       A3: for n be Element of NAT st n in ( dom F) holds (F . n) = ((p . (n -' 1)) * (( power L) . (y,(n -' 1)))) by POLYNOM4:def 2;

      per cases ;

        suppose

         A4: ( len p) > 0 ;

        then

         A5: ( len p) >= ( 0 + 1) by NAT_1: 13;

        then

         A6: ( len p) in ( dom F) by A2, FINSEQ_3: 25;

        p <> ( 0_. L) by A4, POLYNOM4: 3;

        then x <> ( 0. L) by Th28;

        then

         A7: ( len p) = (n + 1) by Th27;



         A8: ((n + 1) -' 1) = n by NAT_D: 34;

        now

          let i be Element of NAT ;

          assume that

           A9: i in ( dom F) and

           A10: i <> (n + 1);

          i in ( Seg ( len F)) by A9, FINSEQ_1:def 3;

          then i >= ( 0 + 1) by FINSEQ_1: 1;

          then (i -' 1) = (i - 1) by XREAL_1: 19, XREAL_0:def 2;

          then (i -' 1) <> n by A10;

          then

           A11: (p . (i -' 1)) = ( 0. L) by Th25;



          thus (F /. i) = (F . i) by A9, PARTFUN1:def 6

          .= (( 0. L) * (( power L) . (y,(i -' 1)))) by A3, A9, A11

          .= ( 0. L);

        end;



        hence ( eval (p,y)) = (F /. (n + 1)) by A1, A7, A5, A2, FINSEQ_3: 25, POLYNOM2: 3

        .= (F . (n + 1)) by A7, A6, PARTFUN1:def 6

        .= ((p . n) * ( power (y,n))) by A3, A7, A5, A8, A2, FINSEQ_3: 25;

      end;

        suppose ( len p) = 0 ;

        then

         A12: p = ( 0_. L) by POLYNOM4: 5;

        then (p . n) = ( 0. L) by ORDINAL1:def 12, FUNCOP_1: 7;

        hence thesis by A12, POLYNOM4: 17;

      end;

    end;

    begin

    reserve p,q for Polynomial of F_Real ;

    set F = F_Real ;

    set z = ( 0_. F);

    set j = ( 1_. F);

    set r0 = ( In ( 0 , REAL ));

    theorem :: POLYDIFF:39



     Th39: for r be Element of F_Real holds ( power (r,n)) = (r |^ n)

    proof

      let r be Element of F;

      defpred P[ Nat] means ( power (r,$1)) = (r |^ $1);

      ( power (r, 0 )) = ( 1_ F) by GROUP_1:def 7;

      then

       A1: P[ 0 ] by NEWTON: 4;

       A2:

      now

        let n be Nat;

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

        assume

         A3: P[n];

        ( power (r,(n + 1))) = (( power (r,n1)) * r) by GROUP_1:def 7

        .= (r |^ (n + 1)) by A3, NEWTON: 6;

        hence P[(n + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: POLYDIFF:40



     Th40: ( #Z n) = ( FPower (( 1. F_Real ),n))

    proof

      reconsider f = ( FPower (( 1. F),n)) as Function of REAL , REAL ;

      ( #Z n) = f

      proof

        let r be Element of REAL ;



        thus (( #Z n) . r) = (r #Z n) by TAYLOR_1:def 1

        .= (r |^ n) by PREPOWER: 36

        .= (( 1. F) * ( power (( In (r,F)),n))) by Th39

        .= (f . r) by POLYNOM5:def 12;

      end;

      hence thesis;

    end;

    theorem :: POLYDIFF:41



     Th41: for r be Element of F_Real holds ( FPower (r,(n + 1))) = (( FPower (r,n)) (#) ( id REAL ))

    proof

      let r be Element of F;

      reconsider f = ( FPower (r,n)) as Function of REAL , REAL ;

      reconsider g = (f (#) ( id REAL )) as Function of F, F;

      now

        let y be Element of F;

        reconsider y1 = y as Element of REAL ;

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



        thus (g . y) = ((f . y1) * (( id REAL ) . y1)) by VALUED_1: 5

        .= ((r * ( power (y,n))) * y) by POLYNOM5:def 12

        .= (r * ((( power F) . (y,n1)) * y))

        .= (r * ( power (y,(n + 1)))) by GROUP_1:def 7;

      end;

      hence thesis by POLYNOM5:def 12;

    end;

    theorem :: POLYDIFF:42



     Th42: for r be Element of F_Real holds ( FPower (r,n)) is differentiable Function of REAL , REAL

    proof

      let r be Element of F;

      defpred P[ Nat] means ( FPower (r,$1)) is differentiable Function of REAL , REAL ;



       A1: P[ 0 ]

      proof

        ( FPower (r, 0 )) = (the carrier of F --> r) by POLYNOM5: 66;

        hence thesis;

      end;



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

      proof

        let n be Nat;

        ( FPower (r,(n + 1))) = (( FPower (r,n)) (#) ( id REAL )) by Th41;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: POLYDIFF:43



     Th43: for r be Element of F_Real holds ( power (r,n)) = (( #Z n) . r)

    proof

      let r be Element of F;



      thus ( power (r,n)) = (( 1. F) * ( power (r,n)))

      .= (( FPower (( 1. F),n)) . r) by POLYNOM5:def 12

      .= (( #Z n) . r) by Th40;

    end;

    definition

      let p;

      :: POLYDIFF:def5

      func poly_diff (p) -> sequence of F_Real means

      : Def5: for n be Nat holds (it . n) = ((p . (n + 1)) * (n + 1));

      existence

      proof

        defpred P[ Element of NAT , object] means $2 = ((p . ($1 + 1)) * ($1 + 1));



         A1: for x be Element of NAT holds ex y be Element of F st P[x, y]

        proof

          let x be Element of NAT ;

          ((p . (x + 1)) * (x + 1)) is Element of F by XREAL_0:def 1;

          hence thesis;

        end;

        consider f be Function of NAT , F such that

         A2: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        let n;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f,g be sequence of F_Real such that

         A3: for n be Nat holds (f . n) = ((p . (n + 1)) * (n + 1)) and

         A4: for n be Nat holds (g . n) = ((p . (n + 1)) * (n + 1));

        let n be Element of NAT ;



        thus (f . n) = ((p . (n + 1)) * (n + 1)) by A3

        .= (g . n) by A4;

      end;

    end

    registration

      let p;

      cluster ( poly_diff p) -> finite-Support;

      coherence

      proof

        consider n be Nat such that

         A1: for i be Nat st i >= n holds (p . i) = ( 0. F) by ALGSEQ_1:def 1;

        take n;

        let i be Nat such that

         A2: i >= n;

        (i + 1) >= (i + 0 ) by XREAL_1: 6;

        then (p . (i + 1)) = ( 0. F) by A1, A2, XXREAL_0: 2;



        hence ( 0. F) = ((p . (i + 1)) * (i + 1))

        .= (( poly_diff p) . i) by Def5;

      end;

    end

    theorem :: POLYDIFF:44



     Th44: p <> ( 0_. F_Real ) implies ( len ( poly_diff p)) = (( len p) - 1)

    proof

      set x = (( len p) - 1);

      set d = ( poly_diff p);

      assume p <> z;

      then

       A1: ( deg p) <> ( - 1) by HURWITZ: 20;

      ( 0 - 1) <= x by XREAL_1: 9;

      then (( - 1) + 1) < (x + 1) by A1;

      then x >= 0 by INT_1: 7;

      then

      reconsider x as Element of NAT by INT_1: 3;



       A2: x is_at_least_length_of d

      proof

        let i be Nat;

        assume i >= x;

        then (i + 1) >= (x + 1) by XREAL_1: 6;

        then (p . (i + 1)) = ( 0. F) by ALGSEQ_1: 8;



        hence ( 0. F) = ((p . (i + 1)) * (i + 1))

        .= (d . i) by Def5;

      end;

      for n st n is_at_least_length_of d holds x <= n

      proof

        let n such that

         A3: n is_at_least_length_of d;

        per cases ;

          suppose x = 0 ;

          hence thesis;

        end;

          suppose x > 0 ;

          then

           A4: x >= ( 0 + 1) by INT_1: 7;

          ( len p) = (x + 1);

          then

           A5: (p . x) <> ( 0. F) by ALGSEQ_1: 10;

          reconsider x1 = (x - 1) as Element of NAT by A4, NAT_1: 21;



           A6: (d . x1) = ((p . (x1 + 1)) * (x1 + 1)) by Def5;

          assume x > n;

          then x >= (n + 1) by INT_1: 7;

          then x1 >= ((n + 1) - 1) by XREAL_1: 9;

          hence contradiction by A5, A3, A6;

        end;

      end;

      hence thesis by A2, ALGSEQ_1:def 3;

    end;

    theorem :: POLYDIFF:45



     Th45: p <> ( 0_. F_Real ) implies ( len p) = (( len ( poly_diff p)) + 1)

    proof

      assume p <> z;

      then ( len ( poly_diff p)) = (( len p) - 1) by Th44;

      hence thesis;

    end;

    theorem :: POLYDIFF:46



     Th46: for p be constant Polynomial of F_Real holds ( poly_diff p) = ( 0_. F_Real )

    proof

      let p be constant Polynomial of F_Real ;

      per cases ;

        suppose p <> z;

        then

         A1: ( len p) = (( len ( poly_diff p)) + 1) by Th45;

        ( deg p) <= 0 by RATFUNC1:def 2;

        then ( len ( poly_diff p)) = 0 by A1;

        then ( deg ( poly_diff p)) = ( - 1);

        hence thesis by HURWITZ: 20;

      end;

        suppose

         A2: p = z;

        let n be Element of NAT ;



        thus (z . n) = ((z . (n + 1)) * (n + 1))

        .= (( poly_diff p) . n) by A2, Def5;

      end;

    end;

    theorem :: POLYDIFF:47



     Th47: ( poly_diff (p + q)) = (( poly_diff p) + ( poly_diff q))

    proof

      let n be Element of NAT ;



       A1: (( poly_diff p) . n) = ((p . (n + 1)) * (n + 1)) by Def5;



       A2: (( poly_diff q) . n) = ((q . (n + 1)) * (n + 1)) by Def5;



       A3: ((p + q) . (n + 1)) = ((p . (n + 1)) + (q . (n + 1))) by NORMSP_1:def 2;



      thus (( poly_diff (p + q)) . n) = (((p + q) . (n + 1)) * (n + 1)) by Def5

      .= ((( poly_diff p) . n) + (( poly_diff q) . n)) by A1, A2, A3

      .= ((( poly_diff p) + ( poly_diff q)) . n) by NORMSP_1:def 2;

    end;

    theorem :: POLYDIFF:48



     Th48: ( poly_diff ( - p)) = ( - ( poly_diff p))

    proof

      let n be Element of NAT ;



       A1: (( poly_diff p) . n) = ((p . (n + 1)) * (n + 1)) by Def5;

      ( dom ( - p)) = NAT by FUNCT_2:def 1;

      then

       A2: (( - p) /. (n + 1)) = ( - (p /. (n + 1))) by VFUNCT_1:def 5;



       A3: ( dom ( - ( poly_diff p))) = NAT by FUNCT_2:def 1;



      thus (( poly_diff ( - p)) . n) = ((( - p) . (n + 1)) * (n + 1)) by Def5

      .= ( - (( poly_diff p) /. n)) by A1, A2

      .= (( - ( poly_diff p)) /. n) by A3, VFUNCT_1:def 5

      .= (( - ( poly_diff p)) . n);

    end;

    theorem :: POLYDIFF:49

    ( poly_diff (p - q)) = (( poly_diff p) - ( poly_diff q))

    proof



      thus ( poly_diff (p - q)) = (( poly_diff p) + ( poly_diff ( - q))) by Th47

      .= (( poly_diff p) - ( poly_diff q)) by Th48;

    end;

    theorem :: POLYDIFF:50



     Th50: ( poly_diff ( Leading-Monomial p)) = (( 0_. F_Real ) +* ((( len p) -' 2),((p . (( len p) -' 1)) * (( len p) -' 1))))

    proof

      set l = ( Leading-Monomial p);

      set m = (( len p) -' 1);

      set k = (( len p) -' 2);

      reconsider a = ((p . m) * m) as Element of F by XREAL_0:def 1;

      set f = (z +* (k,a));

      ( poly_diff l) = f

      proof

        let n be Element of NAT ;



         A1: (( poly_diff l) . n) = ((l . (n + 1)) * (n + 1)) by Def5;



         A2: ( dom z) = NAT ;

        per cases by NAT_1: 53;

          suppose

           A3: ( len p) = 0 or ( len p) = 1;

          (1 - 1) >= 0 ;

          then

           A4: (1 -' 1) = 0 by XREAL_0:def 2;

          (1 - 2) < 0 ;

          then

           A5: k = 0 by A3, XREAL_0:def 2;

          ( 0 -' 1) = 0 ;

          then

           A6: (l . (n + 1)) = ( 0. F) by A3, A4, POLYNOM4:def 1;

          now

            per cases ;

              suppose n = 0 ;

              hence (f . n) = ( 0. F) by A2, A3, A4, A5, FUNCT_7: 31;

            end;

              suppose n <> 0 ;



              hence (f . n) = (z . n) by A5, FUNCT_7: 32

              .= ( 0. F);

            end;

          end;

          hence thesis by A1, A6;

        end;

          suppose

           A7: ( len p) > 1;

          then

           A8: (( len p) - 1) > (1 - 1) by XREAL_1: 14;

          per cases ;

            suppose

             A9: m = (n + 1);

            then

             A10: (l . (n + 1)) = (p . m) by POLYNOM4:def 1;

            k = (m -' 1) by NAT_D: 45;

            then (k + 1) = (n + 1) by A9, NAT_D: 34;

            hence thesis by A1, A2, A9, A10, FUNCT_7: 31;

          end;

            suppose

             A11: m <> (n + 1);

            then

             A12: (l . (n + 1)) = ( 0. F) by POLYNOM4:def 1;



             A13: (( len p) - 2) <> n by A8, A11, XREAL_0:def 2;

            (( len p) - 2) > (1 - 2) by A7, XREAL_1: 14;

            then (( len p) - 2) >= (( - 1) + 1) by INT_1: 7;

            then k = (( len p) - 2) by XREAL_0:def 2;



            hence (f . n) = (z . n) by A13, FUNCT_7: 32

            .= (( poly_diff l) . n) by A1, A12;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYDIFF:51

    for r,s be Element of F_Real holds ( poly_diff <%r, s%>) = <%s%>

    proof

      let r,s be Element of F_Real ;

      let n be Element of NAT ;



       A1: (( poly_diff <%r, s%>) . n) = (( <%r, s%> . (n + 1)) * (n + 1)) by Def5;

      per cases ;

        suppose

         A2: n = 0 ;



        hence (( poly_diff <%r, s%>) . n) = s by A1, POLYNOM5: 38

        .= ( <%s%> . n) by A2, POLYNOM5: 32;

      end;

        suppose n <> 0 ;

        then

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

        (1 + 1) <= (n + 1) by A3, XREAL_1: 6;

        then ( <%r, s%> . (n + 1)) = ( 0. F) by POLYNOM5: 38;

        hence thesis by A1, A3, POLYNOM5: 32;

      end;

    end;

    definition

      let p;

      :: POLYDIFF:def6

      func Eval (p) -> Function of REAL , REAL equals ( Polynomial-Function ( F_Real ,p));

      coherence ;

    end

    registration

      let p;

      cluster ( Eval p) -> differentiable;

      coherence

      proof

        set f = ( Eval p);

        set L = ( RealVectSpace REAL );

        defpred P[ Nat, object] means $2 = ( FPower ((p . ($1 -' 1)),($1 -' 1)));

         A1:

        now

          let n be Nat;

          reconsider x = ( FPower ((p . (n -' 1)),(n -' 1))) as Element of L by FUNCT_2: 9;

          assume n in ( Seg ( len p));

          take x;

          thus P[n, x];

        end;

        consider G be FinSequence of L such that

         A2: ( dom G) = ( Seg ( len p)) and

         A3: for n be Nat st n in ( Seg ( len p)) holds P[n, (G . n)] from FINSEQ_1:sch 5( A1);



         A4: (G | ( len G)) = G by FINSEQ_1: 58;

        reconsider SF = ( Sum G) as Function of REAL , REAL by FUNCT_2: 66;

         A5:

        now

          let x be Element of REAL ;

          reconsider x1 = x as Element of F;

          consider H be FinSequence of F such that

           A6: ( eval (p,x1)) = ( Sum H) and

           A7: ( len H) = ( len p) and

           A8: for n be Element of NAT st n in ( dom H) holds (H . n) = ((p . (n -' 1)) * (( power F) . (x1,(n -' 1)))) by POLYNOM4:def 2;

          defpred P[ Nat] means for SFk be Function of REAL , REAL st SFk = ( Sum (G | $1)) holds ( Sum (H | $1)) = (SFk . x);



           A9: ( len G) = ( len p) by A2, FINSEQ_1:def 3;



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

          proof

            let k be Nat;

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

            assume

             A11: for SFk be Function of REAL , REAL st SFk = ( Sum (G | k)) holds ( Sum (H | k)) = (SFk . x);

            reconsider SFk1 = ( Sum (G | k)) as Function of REAL , REAL by FUNCT_2: 66;

            let SFk be Function of REAL , REAL ;

            assume

             A12: SFk = ( Sum (G | (k + 1)));

            per cases ;

              suppose

               A13: ( len G) > k;

              reconsider g2 = ( FPower ((p . kk),k)) as Function of REAL , REAL ;



               A14: (k + 1) >= 1 by NAT_1: 11;



               A15: (k + 1) <= ( len G) by A13, NAT_1: 13;

              then

               A16: (k + 1) in ( dom G) by NAT_1: 11, FINSEQ_3: 25;



              then

               A17: (G /. (k + 1)) = (G . (k + 1)) by PARTFUN1:def 6

              .= ( FPower ((p . ((k + 1) -' 1)),((k + 1) -' 1))) by A2, A3, A14, A15, FINSEQ_3: 25

              .= ( FPower ((p . kk),((k + 1) -' 1))) by NAT_D: 34

              .= ( FPower ((p . kk),k)) by NAT_D: 34;

              (G | (k + 1)) = ((G | k) ^ <*(G . (k + 1))*>) by A13, FINSEQ_5: 83

              .= ((G | k) ^ <*(G /. (k + 1))*>) by A16, PARTFUN1:def 6;



              then

               A18: SFk = (( Sum (G | k)) + (G /. (k + 1))) by A12, FVSUM_1: 71

              .= (SFk1 + g2) by A17, FUNCSDOM: 28;



               A19: ( Sum (H | k)) = (SFk1 . x) by A11;



               A20: ( dom G) = ( dom H) by A2, A7, FINSEQ_1:def 3;



              then

               A21: (H /. (k + 1)) = (H . (k + 1)) by A16, PARTFUN1:def 6

              .= ((p . ((k + 1) -' 1)) * (( power F) . (x1,((k + 1) -' 1)))) by A8, A20, A16

              .= ((p . kk) * (( power F) . (x1,((k + 1) -' 1)))) by NAT_D: 34

              .= ((p . kk) * ( power (x1,k))) by NAT_D: 34

              .= (( FPower ((p . kk),k)) . x) by POLYNOM5:def 12;

              (H | (k + 1)) = ((H | k) ^ <*(H . (k + 1))*>) by A7, A9, A13, FINSEQ_5: 83

              .= ((H | k) ^ <*(H /. (k + 1))*>) by A20, A16, PARTFUN1:def 6;



              hence ( Sum (H | (k + 1))) = (( Sum (H | k)) + (H /. (k + 1))) by FVSUM_1: 71

              .= (SFk . x) by A21, A18, A19, VALUED_1: 1;

            end;

              suppose

               A22: ( len G) <= k;

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

              then

               A23: (G | (k + 1)) = G & (H | (k + 1)) = H by A7, A9, A22, FINSEQ_1: 58, XXREAL_0: 2;

              (G | k) = G & (H | k) = H by A7, A9, A22, FINSEQ_1: 58;

              hence thesis by A11, A12, A23;

            end;

          end;



           A24: P[ 0 ]

          proof

            let SFk be Function of REAL , REAL ;



             A25: (G | 0 ) = ( <*> the carrier of L);

            assume SFk = ( Sum (G | 0 ));



            then

             A26: SFk = ( 0. L) by A25, RLVECT_1: 43

            .= ( REAL --> r0);

            (H | 0 ) = ( <*> the carrier of F);



            hence ( Sum (H | 0 )) = ( 0. F) by RLVECT_1: 43

            .= (SFk . x) by A26;

          end;



           A27: for k be Nat holds P[k] from NAT_1:sch 2( A24, A10);



           A28: ( Sum (G | ( len G))) = SF by FINSEQ_1: 58;



          thus (f . x) = ( Sum H) by A6, POLYNOM5:def 13

          .= ( Sum (H | ( len H))) by FINSEQ_1: 58

          .= (SF . x) by A7, A9, A27, A28;

        end;

        defpred P[ Nat] means for g be PartFunc of REAL , REAL st g = ( Sum (G | $1)) holds g is differentiable;



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

        proof

          let k be Nat;

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

          reconsider g1 = ( Sum (G | k)) as Function of REAL , REAL by FUNCT_2: 66;

          assume

           A30: for g be PartFunc of REAL , REAL st g = ( Sum (G | k)) holds g is differentiable;

          then

           A31: g1 is differentiable;

          let g be PartFunc of REAL , REAL ;

          assume

           A32: g = ( Sum (G | (k + 1)));

          per cases ;

            suppose

             A33: ( len G) > k;

            (k + 1) <= ( len G) by A33, NAT_1: 13;

            then

             A34: (k + 1) in ( dom G) by NAT_1: 11, FINSEQ_3: 25;



            then

             A35: (G /. (k + 1)) = (G . (k + 1)) by PARTFUN1:def 6

            .= ( FPower ((p . ((k + 1) -' 1)),((k + 1) -' 1))) by A2, A3, A34

            .= ( FPower ((p . kk),((k + 1) -' 1))) by NAT_D: 34

            .= ( FPower ((p . kk),k)) by NAT_D: 34;



             A36: ( FPower ((p . kk),k)) is differentiable Function of REAL , REAL by Th42;

            (G | (k + 1)) = ((G | k) ^ <*(G . (k + 1))*>) by A33, FINSEQ_5: 83

            .= ((G | k) ^ <*(G /. (k + 1))*>) by A34, PARTFUN1:def 6;



            then g = (( Sum (G | k)) + (G /. (k + 1))) by A32, FVSUM_1: 71

            .= (g1 + ( FPower ((p . kk),k))) by A35, FUNCSDOM: 28;

            hence thesis by A31, A36;

          end;

            suppose

             A37: ( len G) <= k;

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



            then (G | (k + 1)) = G by A37, FINSEQ_1: 58, XXREAL_0: 2

            .= (G | k) by A37, FINSEQ_1: 58;

            hence thesis by A30, A32;

          end;

        end;



         A38: P[ 0 ]

        proof

          let g be PartFunc of REAL , REAL ;



           A39: (G | 0 ) = ( <*> the carrier of L);

          assume g = ( Sum (G | 0 ));



          then g = ( 0. L) by A39, RLVECT_1: 43

          .= ( REAL --> r0);

          hence thesis;

        end;

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

        hence thesis by A4, A5, FUNCT_2: 63;

      end;

    end

    theorem :: POLYDIFF:52



     Th52: ( Eval ( 0_. F_Real )) = ( REAL --> 0 )

    proof

      ( Eval z) = ( REAL --> r0)

      proof

        let r be Element of REAL ;



        thus (( Eval z) . r) = ( eval (z,( In (r,F)))) by POLYNOM5:def 13

        .= r0 by POLYNOM4: 17

        .= (( REAL --> r0) . r);

      end;

      hence thesis;

    end;

    theorem :: POLYDIFF:53



     Th53: for r be Element of F_Real holds ( Eval <%r%>) = ( REAL --> r)

    proof

      let r be Element of F;

      ( Eval <%r%>) = ( REAL --> ( In (r, REAL )))

      proof

        let a be Element of REAL ;



        thus (( Eval <%r%>) . a) = ( eval ( <%r%>,( In (a,F)))) by POLYNOM5:def 13

        .= r by POLYNOM5: 37

        .= (( REAL --> ( In (r, REAL ))) . a);

      end;

      hence thesis;

    end;

     Lm2:

    now

      let r be Element of F;

      ( Eval <%r%>) = ( REAL --> ( In (r, REAL ))) by Th53;

      hence (( Eval <%r%>) `| ) = ( REAL --> 0 ) by Th11;

    end;

    theorem :: POLYDIFF:54



     Th54: p is constant implies (( Eval p) `| ) = ( REAL --> 0 )

    proof

      assume p is constant;

      then p = ( 0_. F) or p = <%(p . 0 )%> by Th23;

      hence thesis by Th52, Lm2, Th11;

    end;

    theorem :: POLYDIFF:55



     Th55: ( Eval (p + q)) = (( Eval p) + ( Eval q))

    proof

      let r be Element of REAL ;

      set s = ( In (r,F));

      (( Eval p) . r) = ( eval (p,s)) & (( Eval q) . r) = ( eval (q,s)) by POLYNOM5:def 13;



      hence ((( Eval p) + ( Eval q)) . r) = (( eval (p,s)) + ( eval (q,s))) by VALUED_1: 1

      .= ( eval ((p + q),s)) by POLYNOM4: 19

      .= (( Eval (p + q)) . r) by POLYNOM5:def 13;

    end;

    theorem :: POLYDIFF:56



     Th56: ( Eval ( - p)) = ( - ( Eval p))

    proof

      let r be Element of REAL ;

      set s = ( In (r,F));

      (( Eval p) . r) = ( eval (p,s)) by POLYNOM5:def 13;



      hence (( - ( Eval p)) . r) = ( - ( eval (p,s))) by VALUED_1: 8

      .= ( eval (( - p),s)) by POLYNOM4: 20

      .= (( Eval ( - p)) . r) by POLYNOM5:def 13;

    end;

    theorem :: POLYDIFF:57

    ( Eval (p - q)) = (( Eval p) - ( Eval q))

    proof



      thus ( Eval (p - q)) = (( Eval p) + ( Eval ( - q))) by Th55

      .= (( Eval p) - ( Eval q)) by Th56;

    end;

    theorem :: POLYDIFF:58

    ( Eval ( Leading-Monomial p)) = ( FPower ((p . (( len p) -' 1)),(( len p) -' 1)))

    proof

      set l = ( Leading-Monomial p);

      set m = (( len p) -' 1);

      reconsider f = ( FPower ((p . m),m)) as Function of REAL , REAL ;

      ( Eval l) = f

      proof

        let r be Element of REAL ;



        thus (( Eval l) . r) = ( eval (l,( In (r,F)))) by POLYNOM5:def 13

        .= ((p . m) * ( power (( In (r,F)),m))) by POLYNOM4: 22

        .= (f . r) by POLYNOM5:def 12;

      end;

      hence thesis;

    end;

    theorem :: POLYDIFF:59



     Th59: ( Eval ( Leading-Monomial p)) = ((p . (( len p) -' 1)) (#) ( #Z (( len p) -' 1)))

    proof

      set l = ( Leading-Monomial p);

      set m = (( len p) -' 1);

      set f = ((p . m) (#) ( #Z m));

      ( Eval l) = f

      proof

        let r be Element of REAL ;



         A1: ( power (( In (r,F)),m)) = (r |^ m) by Th39

        .= (r #Z m) by PREPOWER: 36

        .= (( #Z m) . r) by TAYLOR_1:def 1;



        thus (( Eval l) . r) = ( eval (l,( In (r,F)))) by POLYNOM5:def 13

        .= ((p . m) * ( power (( In (r,F)),m))) by POLYNOM4: 22

        .= (f . r) by A1, VALUED_1: 6;

      end;

      hence thesis;

    end;

    theorem :: POLYDIFF:60



     Th60: for r be Element of F_Real holds ( Eval ( seq (n,r))) = (r (#) ( #Z n))

    proof

      let r be Element of F_Real ;

      let a be Element of REAL ;

      set p = ( seq (n,r));

      set x = ( In (a,F));



       A1: (p . n) = r by Th24;



       A2: ( power (x,n)) = (( #Z n) . a) by Th43;



      thus (( Eval p) . a) = ( eval (p,x)) by POLYNOM5:def 13

      .= ((p . n) * ( power (x,n))) by Th38

      .= ((r (#) ( #Z n)) . a) by A1, A2, VALUED_1: 6;

    end;



     Lm3: (( Eval ( Leading-Monomial p)) `| ) = ( Eval ( poly_diff ( Leading-Monomial p)))

    proof

      set l = ( Leading-Monomial p);

      set m = (( len p) -' 1);

      set k = (( len p) -' 2);

      reconsider f = ( FPower ((p . m),m)) as Function of REAL , REAL ;

      reconsider a = ((p . m) * m) as Element of F by XREAL_0:def 1;



       A1: ( poly_diff l) = ( seq (k,a)) by Th50;



       A2: (( #Z m) `| ) = (m (#) ( #Z (m - 1))) by Th13;

      ( len p) <= (2 - 1) or ( len p) >= 2 by INT_1: 52;

      per cases by NAT_1: 25;

        suppose ( len p) = 0 or ( len p) = 1;

        then

         A3: p = z or p = <%(p . 0 )%> by ALGSEQ_1:def 5;

        then ( poly_diff l) = z by Th46;

        hence thesis by A3, Th52, Th54;

      end;

        suppose

         A4: 2 <= ( len p);

        then

         A5: (( len p) -' 2) = (( len p) - 2) by XREAL_1: 233;

        (( len p) -' 1) = (( len p) - 1) by A4, XXREAL_0: 2, XREAL_1: 233;

        then

         A6: (a (#) ( #Z (m - 1))) = ( Eval ( seq (k,a))) by A5, Th60;

        ( Eval l) = ((p . m) (#) ( #Z m)) by Th59;



        hence (( Eval l) `| ) = ((p . m) (#) (( #Z m) `| )) by Th19

        .= ( Eval ( poly_diff l)) by A1, A2, A6, RFUNCT_1: 17;

      end;

    end;

    theorem :: POLYDIFF:61



     Th61: (( Eval p) `| ) = ( Eval ( poly_diff p))

    proof

      set f = (( Eval p) `| );

      set g = ( Eval ( poly_diff p));

      defpred P[ Nat] means for p st ( len p) <= $1 holds (( Eval p) `| ) = ( Eval ( poly_diff p));



       A1: P[ 0 ]

      proof

        let p;

        assume ( len p) <= 0 ;

        then ( len p) = 0 ;

        then

         A2: p = z by POLYNOM4: 5;

        ( poly_diff z) = z by Th46;

        hence thesis by A2, Th52, Th54;

      end;



       A3: P[n] implies P[(n + 1)]

      proof

        assume that

         A4: P[n];

        let p such that

         A5: ( len p) <= (n + 1);

        set m = (( len p) -' 1);

        set q = (p || m);

        now

          per cases ;

            suppose p <> z;

            hence ( len q) < (n + 1) by A5, Th36, XXREAL_0: 2;

          end;

            suppose p = z;

            hence ( len q) < (n + 1) by POLYNOM4: 3;

          end;

        end;

        then

         A6: (( Eval q) `| ) = ( Eval ( poly_diff q)) by A4, NAT_1: 13;

        set l = ( Leading-Monomial p);



         A7: (q + l) = p by Th37;



         A8: ( poly_diff (q + l)) = (( poly_diff q) + ( poly_diff l)) by Th47;



         A9: (( Eval l) `| ) = ( Eval ( poly_diff l)) by Lm3;



         A10: ( Eval (( poly_diff q) + ( poly_diff l))) = (( Eval ( poly_diff q)) + ( Eval ( poly_diff l))) by Th55;

        ( Eval (q + l)) = (( Eval q) + ( Eval l)) by Th55;

        hence thesis by A6, A7, A8, A9, A10, Th14;

      end;



       A11: P[n] from NAT_1:sch 2( A1, A3);

      ( len p) = ( len p);

      hence thesis by A11;

    end;

    registration

      let p;

      cluster (( Eval p) `| ) -> differentiable;

      coherence

      proof

        (( Eval p) `| ) = ( Eval ( poly_diff p)) by Th61;

        hence thesis;

      end;

    end