let n be Nat; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) ; :: thesis: 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 ) ; :: thesis: verum