:: Derivation of Commutative Rings \& {L}eibnitz Formula for Power of Derivation
:: by Yasushige Watase
::
:: Received March 30, 2021
:: Copyright (c) 2021 Association of Mizar Users

:: <section0>Preliminaries</section0>
theorem Th1: :: RINGDER1:1
for L being non empty right_complementable associative Abelian add-associative right_zeroed distributive left_zeroed doubleLoopStr
for a, b being Element of L
for n being Nat holds (n * a) + (n * b) = n * (a + b)
proof end;

theorem :: RINGDER1:2
for L being non empty right_complementable associative Abelian add-associative right_zeroed distributive left_zeroed doubleLoopStr
for a, b being Element of L
for n being Nat holds (n * a) * b = a * (n * b)
proof end;

theorem Th3: :: RINGDER1:3
for L being non empty right_complementable associative Abelian add-associative right_zeroed distributive left_zeroed doubleLoopStr
for n being Nat holds n * (0. L) = 0. L
proof end;

theorem :: RINGDER1:4
for L being non empty right_complementable associative Abelian add-associative right_zeroed distributive left_zeroed doubleLoopStr
for n being Nat holds (0. L) * n = 0. L
proof end;

definition
let R be non degenerated comRing;
let IT be Function of R,R;
attr IT is derivation means :Def1: :: RINGDER1:def 1
for x, y being Element of R holds
( IT . (x + y) = (IT . x) + (IT . y) & IT . (x * y) = (x * (IT . y)) + (y * (IT . x)) );
end;

:: deftheorem Def1 defines derivation RINGDER1:def 1 :
for R being non degenerated comRing
for IT being Function of R,R holds
( IT is derivation iff for x, y being Element of R holds
( IT . (x + y) = (IT . x) + (IT . y) & IT . (x * y) = (x * (IT . y)) + (y * (IT . x)) ) );

registration
let R be non degenerated comRing;
cluster Function-like quasi_total derivation -> additive for Element of K10(K11( the carrier of R, the carrier of R));
coherence
for b1 being Function of R,R st b1 is derivation holds
;
end;

registration
let R be non degenerated comRing;
cluster non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like total quasi_total derivation for Element of K10(K11( the carrier of R, the carrier of R));
existence
ex b1 being Function of R,R st b1 is derivation
proof end;
end;

definition
let R be non degenerated comRing;
mode Derivation of R is derivation Function of R,R;
end;

definition
let R be non degenerated comRing;
func Der R -> Subset of (Funcs (([#] R),([#] R))) equals :: RINGDER1:def 2
{ f where f is Function of R,R : f is derivation } ;
coherence
{ f where f is Function of R,R : f is derivation } is Subset of (Funcs (([#] R),([#] R)))
proof end;
end;

:: deftheorem defines Der RINGDER1:def 2 :
for R being non degenerated comRing holds Der R = { f where f is Function of R,R : f is derivation } ;

registration
let R be non degenerated comRing;
cluster Der R -> non empty ;
correctness
coherence
not Der R is empty
;
proof end;
end;

theorem Th5: :: RINGDER1:5
for R being non degenerated comRing
for D being Derivation of R holds
( D . (1. R) = 0. R & D . (0. R) = 0. R )
proof end;

theorem Th6: :: RINGDER1:6
for R being non degenerated comRing
for D being Derivation of R
for n being Nat
for x being Element of R holds D . (n * x) = n * (D . x)
proof end;

theorem Th7: :: RINGDER1:7
for R being non degenerated comRing
for m being Nat
for x being Element of R
for D being Derivation of R holds D . (x |^ (m + 1)) = (m + 1) * ((x |^ m) * (D . x))
proof end;

::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Power of Derivation D|^(n+1).f = D.(D|^n.f)
::::::::::::::::::::::::::::::::::::::::::::::::::::
:: D|^2 is Function of the carrier of R,the carrier of R;
:: D|^3 is Function of the carrier of R,the carrier of R;
:: D|^0 = id R by VECTSP11:18;
:: R is non empty & D is Function of R,R;
:: dom D = the carrier of R by FUNCT_2:def 1;
:::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem Th8: :: RINGDER1:8
for R being non degenerated comRing
for n being Nat
for D being Derivation of R holds
( D |^ (n + 1) = D * (D |^ n) & dom D = the carrier of R & dom (D |^ n) = the carrier of R & D |^ n is the carrier of b1 -valued Function )
proof end;

theorem Th9: :: RINGDER1:9
for R being non degenerated comRing
for D being Derivation of R
for n being Nat
for x being Element of R holds (D |^ (n + 1)) . x = D . ((D |^ n) . x)
proof end;

::::::::::::::::::::::::::::::::::::::::
::: D.(a/b) = (b*D.a - a*F.b)/b^2
::::::::::::::::::::::::::::::::::::::::
theorem :: RINGDER1:10
for R being non degenerated comRing
for D being Derivation of R
for x, y, z being Element of R st z * y = 1. R holds
(y |^ 2) * (D . (x * z)) = (y * (D . x)) - (x * (D . y))
proof end;

definition
let R be non degenerated comRing;
let s be FinSequence of the carrier of R;
let h be Function of R,R;
:: original: *
redefine func h * s -> FinSequence of the carrier of R;
coherence
s * h is FinSequence of the carrier of R
by FINSEQ_2:32;
end;

theorem Th11: :: RINGDER1:11
for R being non degenerated comRing
for h being Function of R,R
for s being FinSequence of the carrier of R st h is additive holds
h . (Sum s) = Sum (h * s)
proof end;

::::::::::::::::::::::::::::::::::::::::::::::::
::: Formula
::: (f1 + f2 +...+fn)' = f1' + f2' +...+ fn'
::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: RINGDER1:12
for R being non degenerated comRing
for D being Derivation of R
for s being FinSequence of the carrier of R holds D . (Sum s) = Sum (D * s) by Th11;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Formula
:: (f1*f2*...*fn)' = f1'*f2...*fn + f1*f2'*..*fn +....+ f1*f2*f3*..*fn'
:: D.(Product s) = (f1*f2*...*fn)'
:: Sum DProd(D,s) = f1'*f2...fn + f1*f2'*....fn + f1*f2*f3'..
:: here DProd(D,s) = f1*..*D.fi*...*fn = Product( replace(s,i,D.fi))
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R be non degenerated comRing;
let D be Derivation of R;
let s be FinSequence of the carrier of R;
func DProd (D,s) -> FinSequence of the carrier of R means :Def3: :: RINGDER1:def 3
( len it = len s & ( for i being Nat st i in dom it holds
it . i = Product (Replace (s,i,(D . (s /. i)))) ) );
existence
ex b1 being FinSequence of the carrier of R st
( len b1 = len s & ( for i being Nat st i in dom b1 holds
b1 . i = Product (Replace (s,i,(D . (s /. i)))) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of R st len b1 = len s & ( for i being Nat st i in dom b1 holds
b1 . i = Product (Replace (s,i,(D . (s /. i)))) ) & len b2 = len s & ( for i being Nat st i in dom b2 holds
b2 . i = Product (Replace (s,i,(D . (s /. i)))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines DProd RINGDER1:def 3 :
for R being non degenerated comRing
for D being Derivation of R
for s, b4 being FinSequence of the carrier of R holds
( b4 = DProd (D,s) iff ( len b4 = len s & ( for i being Nat st i in dom b4 holds
b4 . i = Product (Replace (s,i,(D . (s /. i)))) ) ) );

theorem Th13: :: RINGDER1:13
for R being non degenerated comRing
for D being Derivation of R
for s being FinSequence of the carrier of R st len s = 1 holds
Sum (DProd (D,s)) = D . ()
proof end;

theorem :: RINGDER1:14
for R being non degenerated comRing
for D being Derivation of R
for t being FinSequence of the carrier of R st len t >= 1 holds
Sum (DProd (D,t)) = D . ()
proof end;

:: <section2>Proof of Leibnitz Formula for Power of Derivations</section2>
:::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Leibniz Formula for power of a derivation of a commutative ring
:: LBZ(D,n,x,y) = <* nC0*(D^n.x), nC1*(D^(n-1).x)*(D.y),......*>
:: D^n(x+y) = nC0*(D^n.x) + nC1*(D^(n-1).x)*(D.y) +
:: D^n(x+y) = Sum LBZ(D,n,x,y)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R be non degenerated comRing;
let D be Derivation of R;
let n be Nat;
let x, y be Element of R;
func LBZ (D,n,x,y) -> FinSequence of the carrier of R means :Def4: :: RINGDER1:def 4
( len it = n + 1 & ( for i being Nat st i in dom it holds
it . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) );
existence
ex b1 being FinSequence of the carrier of R st
( len b1 = n + 1 & ( for i being Nat st i in dom b1 holds
b1 . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of R st len b1 = n + 1 & ( for i being Nat st i in dom b1 holds
b1 . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) & len b2 = n + 1 & ( for i being Nat st i in dom b2 holds
b2 . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines LBZ RINGDER1:def 4 :
for R being non degenerated comRing
for D being Derivation of R
for n being Nat
for x, y being Element of R
for b6 being FinSequence of the carrier of R holds
( b6 = LBZ (D,n,x,y) iff ( len b6 = n + 1 & ( for i being Nat st i in dom b6 holds
b6 . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) ) );

theorem Th15: :: RINGDER1:15
for R being non degenerated comRing
for x, y being Element of R
for D being Derivation of R holds LBZ (D,0,x,y) = <*(x * y)*>
proof end;

theorem Th16: :: RINGDER1:16
for R being non degenerated comRing
for x, y being Element of R
for D being Derivation of R holds LBZ (D,1,x,y) = <*(y * (D . x)),(x * (D . y))*>
proof end;

definition
let R be non degenerated comRing;
let D be Derivation of R;
let m be Nat;
let x, y be Element of R;
func LBZ0 (D,m,x,y) -> FinSequence of the carrier of R means :Def5: :: RINGDER1:def 5
( len it = m & ( for i being Nat st i in dom it holds
it . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) );
existence
ex b1 being FinSequence of the carrier of R st
( len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of R st len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) & len b2 = m & ( for i being Nat st i in dom b2 holds
b2 . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines LBZ0 RINGDER1:def 5 :
for R being non degenerated comRing
for D being Derivation of R
for m being Nat
for x, y being Element of R
for b6 being FinSequence of the carrier of R holds
( b6 = LBZ0 (D,m,x,y) iff ( len b6 = m & ( for i being Nat st i in dom b6 holds
b6 . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) ) );

definition
let R be non degenerated comRing;
let D be Derivation of R;
let m be Nat;
let x, y be Element of R;
func LBZ1 (D,m,x,y) -> FinSequence of the carrier of R means :Def6: :: RINGDER1:def 6
( len it = m & ( for i being Nat st i in dom it holds
it . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) );
existence
ex b1 being FinSequence of the carrier of R st
( len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of R st len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) & len b2 = m & ( for i being Nat st i in dom b2 holds
b2 . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines LBZ1 RINGDER1:def 6 :
for R being non degenerated comRing
for D being Derivation of R
for m being Nat
for x, y being Element of R
for b6 being FinSequence of the carrier of R holds
( b6 = LBZ1 (D,m,x,y) iff ( len b6 = m & ( for i being Nat st i in dom b6 holds
b6 . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) ) );

definition
let R be non degenerated comRing;
let D be Derivation of R;
let m be Nat;
let x, y be Element of R;
func LBZ2 (D,m,x,y) -> FinSequence of the carrier of R means :Def7: :: RINGDER1:def 7
( len it = m & ( for i being Nat st i in dom it holds
it . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) );
existence
ex b1 being FinSequence of the carrier of R st
( len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of R st len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) & len b2 = m & ( for i being Nat st i in dom b2 holds
b2 . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines LBZ2 RINGDER1:def 7 :
for R being non degenerated comRing
for D being Derivation of R
for m being Nat
for x, y being Element of R
for b6 being FinSequence of the carrier of R holds
( b6 = LBZ2 (D,m,x,y) iff ( len b6 = m & ( for i being Nat st i in dom b6 holds
b6 . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) ) );

theorem :: RINGDER1:17
for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds D . (Sum (LBZ0 (D,n,x,y))) = Sum (D * (LBZ0 (D,n,x,y))) by Th11;

theorem Th18: :: RINGDER1:18
for R being non degenerated comRing
for m being Nat
for x, y being Element of R
for D being Derivation of R holds LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))
proof end;

theorem Th19: :: RINGDER1:19
for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds Sum (LBZ0 (D,n,x,y)) = (Sum (LBZ1 (D,n,x,y))) + (Sum (LBZ2 (D,n,x,y)))
proof end;

theorem Th20: :: RINGDER1:20
for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds D * (LBZ0 (D,n,x,y)) = (Del ((LBZ2 (D,(n + 1),x,y)),(n + 1))) + (Del ((LBZ1 (D,(n + 1),x,y)),1))
proof end;

Lm1: for R being non degenerated comRing
for x, y being Element of R
for D being Derivation of R
for n being Nat st 1 <= n holds
(LBZ1 (D,n,x,y)) /. 1 = ((D |^ n) . x) * (D . y)

proof end;

Lm2: for R being non degenerated comRing
for x, y being Element of R
for D being Derivation of R
for n being Nat st 1 <= n holds
(LBZ2 (D,n,x,y)) /. n = (D . x) * ((D |^ n) . y)

proof end;

theorem Th21: :: RINGDER1:21
for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds Sum (D * (LBZ0 (D,n,x,y))) = ((- ((LBZ1 (D,(n + 1),x,y)) /. 1)) + (Sum (LBZ0 (D,(n + 1),x,y)))) - ((LBZ2 (D,(n + 1),x,y)) /. (n + 1))
proof end;

theorem Th22: :: RINGDER1:22
for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>
proof end;

theorem Th23: :: RINGDER1:23
for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds Sum ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) = ((((D |^ (n + 1)) . x) * y) + (Sum (LBZ0 (D,n,x,y)))) + (x * ((D |^ (n + 1)) . y))
proof end;

theorem Th24: :: RINGDER1:24
for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds D . (Sum (LBZ (D,(n + 1),x,y))) = Sum (LBZ (D,(n + 2),x,y))
proof end;

:::::::::::::::::::::::::::::::::::::::::::::::::
:: Leibniz Formula for Power of Derivation.
:::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: RINGDER1:25
for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds (D |^ n) . (x * y) = Sum (LBZ (D,n,x,y))
proof end;

::<section3>Example of Derivation of Polynomial Ring over a Commutative Ring</section3>
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:::: formalize derivation of Polynom-Ring R.
:::: start with same fashion of poly_diff of POLYDIFF1:
:::: However resource of Def of poly_diff of POLYDIFF1 cannot be imported
:::: with the environment of this article technically.
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Relations between
::: Element of the carrier of Polynom-Ring R and Polynomial of R
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R be non degenerated comRing;
let f be Function of (),();
let p be Element of the carrier of ();
:: original: .
redefine func f . p -> Element of the carrier of ();
coherence
f . p is Element of the carrier of ()
proof end;
end;

definition
let R be Ring;
func Der1 R -> Function of (),() means :Def8: :: RINGDER1:def 8
for f being Element of the carrier of ()
for i being Nat holds (it . f) . i = (i + 1) * (f . (i + 1));
existence
ex b1 being Function of (),() st
for f being Element of the carrier of ()
for i being Nat holds (b1 . f) . i = (i + 1) * (f . (i + 1))
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for f being Element of the carrier of ()
for i being Nat holds (b1 . f) . i = (i + 1) * (f . (i + 1)) ) & ( for f being Element of the carrier of ()
for i being Nat holds (b2 . f) . i = (i + 1) * (f . (i + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Der1 RINGDER1:def 8 :
for R being Ring
for b2 being Function of (),() holds
( b2 = Der1 R iff for f being Element of the carrier of ()
for i being Nat holds (b2 . f) . i = (i + 1) * (f . (i + 1)) );

registration
let R be non degenerated comRing;
coherence
Der1 R is additive
proof end;
end;

theorem :: RINGDER1:26
for R being domRing
for f being Element of the carrier of ()
for f1 being Polynomial of R st f = f1 & f1 is constant holds
(Der1 R) . f = 0_. R
proof end;

Lm3: for R being domRing
for a being Element of R holds a | R = <%a%>

proof end;

theorem Th27: :: RINGDER1:27
for R being domRing
for a being Element of R
for i being Nat
for p being Element of the carrier of () holds ((a | R) *' p) . i = a * (p . i)
proof end;

theorem Th28: :: RINGDER1:28
for R being domRing
for f, g being Element of the carrier of ()
for a being Element of R st f = a | R holds
(Der1 R) . (f * g) = (a | R) *' ((Der1 R) . g)
proof end;

theorem Th29: :: RINGDER1:29
for R being domRing
for f being Element of the carrier of ()
for a being Element of R st f = anpoly (a,0) holds
(Der1 R) . f = 0_. R
proof end;

theorem Th30: :: RINGDER1:30
for R being domRing
for f being Element of the carrier of ()
for a being Element of R st f = anpoly (a,1) holds
(Der1 R) . f = anpoly (a,0)
proof end;

theorem Th31: :: RINGDER1:31
for R being domRing
for p, q being Polynomial of R st p = anpoly ((1. R),1) holds
for i being Element of NAT holds
( (p *' q) . (i + 1) = q . i & (p *' q) . 0 = 0. R )
proof end;

theorem Th32: :: RINGDER1:32
for R being domRing
for f, g being Element of the carrier of () st f = anpoly ((1. R),1) holds
(Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))
proof end;

Lm4: for R being domRing
for p being non constant Polynomial of R holds LM p = ((p . (deg p)) * (anpoly ((1. R),((deg p) -' 1)))) *' (anpoly ((1. R),1))

proof end;

theorem :: RINGDER1:33
for R being domRing
for f, g being constant Element of the carrier of () holds (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))
proof end;

theorem Th34: :: RINGDER1:34
for R being domRing
for f, g being Element of the carrier of () st f is constant holds
(Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))
proof end;

theorem Th35: :: RINGDER1:35
for R being domRing
for x, y being Element of the carrier of () st not x is constant holds
(Der1 R) . (x * y) = (((Der1 R) . x) * y) + (x * ((Der1 R) . y))
proof end;

theorem Th36: :: RINGDER1:36
for R being domRing
for f, g being Element of the carrier of () holds (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))
proof end;

registration
let R be domRing;
coherence by ;
end;

theorem Th37: :: RINGDER1:37
for R being domRing
for x being Element of ()
for f being Polynomial of R st x = f holds
for n being Nat holds x |^ n = f `^ n
proof end;

theorem :: RINGDER1:38
for n being Nat
for R being domRing
for x being Element of () st x = anpoly ((1. R),1) holds
ex y being Element of () st
( y = anpoly ((1. R),n) & (Der1 R) . (x |^ (n + 1)) = (n + 1) * y )
proof end;

definition
let p be Polynomial of F_Real;
func poly_diff p -> sequence of F_Real means :Def9: :: RINGDER1:def 9
for n being Nat holds it . n = (p . (n + 1)) * (n + 1);
existence
ex b1 being sequence of F_Real st
for n being Nat holds b1 . n = (p . (n + 1)) * (n + 1)
proof end;
uniqueness
for b1, b2 being sequence of F_Real st ( for n being Nat holds b1 . n = (p . (n + 1)) * (n + 1) ) & ( for n being Nat holds b2 . n = (p . (n + 1)) * (n + 1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines poly_diff RINGDER1:def 9 :
for p being Polynomial of F_Real
for b2 being sequence of F_Real holds
( b2 = poly_diff p iff for n being Nat holds b2 . n = (p . (n + 1)) * (n + 1) );

theorem :: RINGDER1:39
for p0 being Element of
for p being Polynomial of F_Real st p0 = p holds
poly_diff p = () . p0
proof end;