let n be Nat; for R being domRing
for x being Element of (Polynom-Ring R) st x = anpoly ((1. R),1) holds
ex y being Element of (Polynom-Ring R) st
( y = anpoly ((1. R),n) & (Der1 R) . (x |^ (n + 1)) = (n + 1) * y )
let R be domRing; for x being Element of (Polynom-Ring R) st x = anpoly ((1. R),1) holds
ex y being Element of (Polynom-Ring R) st
( y = anpoly ((1. R),n) & (Der1 R) . (x |^ (n + 1)) = (n + 1) * y )
let x be Element of (Polynom-Ring R); ( x = anpoly ((1. R),1) implies ex y being Element of (Polynom-Ring R) st
( y = anpoly ((1. R),n) & (Der1 R) . (x |^ (n + 1)) = (n + 1) * y ) )
assume A1:
x = anpoly ((1. R),1)
; ex y being Element of (Polynom-Ring R) st
( y = anpoly ((1. R),n) & (Der1 R) . (x |^ (n + 1)) = (n + 1) * y )
reconsider x1 = anpoly ((1. R),1) as Polynomial of R ;
A2: <%(0. R),(1. R)%> =
<%(0. R),(1. R)%> `^ 1
by POLYNOM5:16
.=
x1
by FIELD_1:12
;
reconsider D = Der1 R as Derivation of (Polynom-Ring R) ;
D . x =
anpoly ((1. R),0)
by A1, Th30
.=
1_. R
;
then
( x |^ n = x1 `^ n & D . x = 1_. R )
by A1, Th37;
then A3: (x |^ n) * (D . x) =
(x1 `^ n) *' (1_. R)
by POLYNOM3:def 10
.=
anpoly ((1. R),n)
by A2, FIELD_1:12
;
reconsider y = anpoly ((1. R),n) as Element of (Polynom-Ring R) by POLYNOM3:def 10;
D . (x |^ (n + 1)) = (n + 1) * y
by A3, Th7;
hence
ex y being Element of (Polynom-Ring R) st
( y = anpoly ((1. R),n) & (Der1 R) . (x |^ (n + 1)) = (n + 1) * y )
; verum