let R be domRing; :: thesis: for f being Element of the carrier of (Polynom-Ring R)
for a being Element of R st f = anpoly (a,0) holds
(Der1 R) . f = 0_. R
let f be Element of the carrier of (Polynom-Ring R); :: thesis: for a being Element of R st f = anpoly (a,0) holds
(Der1 R) . f = 0_. R
let a be Element of R; :: thesis: ( f = anpoly (a,0) implies (Der1 R) . f = 0_. R )
assume A1: f = anpoly (a,0) ; :: thesis: (Der1 R) . f = 0_. R
for n being Element of NAT holds ((Der1 R) . f) . n = (0_. R) . n
proof
let n be Element of NAT ; :: thesis: ((Der1 R) . f) . n = (0_. R) . n
((Der1 R) . f) . n = (n + 1) * ((anpoly (a,0)) . (n + 1)) by A1, Def8
.= (n + 1) * (0. R) by POLYDIFF:25
.= (0_. R) . n by Th3 ;
hence ((Der1 R) . f) . n = (0_. R) . n ; :: thesis: verum
end;
hence (Der1 R) . f = 0_. R ; :: thesis: verum