let R be domRing; :: thesis: for f being Element of the carrier of (Polynom-Ring R)
for f1 being Polynomial of R st f = f1 & f1 is constant holds
(Der1 R) . f = 0_. R
let f be Element of the carrier of (Polynom-Ring R); :: thesis: for f1 being Polynomial of R st f = f1 & f1 is constant holds
(Der1 R) . f = 0_. R
let f1 be Polynomial of R; :: thesis: ( f = f1 & f1 is constant implies (Der1 R) . f = 0_. R )
assume A1: ( f = f1 & f1 is constant ) ; :: thesis: (Der1 R) . f = 0_. R
for i being Element of NAT holds ((Der1 R) . f) . i = (0_. R) . i

proof

let i be Element of NAT ; :: thesis: ((Der1 R) . f) . i = (0_. R) . i
((Der1 R) . f) . i = (i + 1) * (f1 . (i + 1)) by A1, Def8
.= (i + 1) * (0. R) by ALGSEQ_1:8, A1, XREAL_1:20
.= (0_. R) . i by Th3 ;
hence ((Der1 R) . f) . i = (0_. R) . i ; :: thesis: verum

end;

hence (Der1 R) . f = 0_. R ; :: thesis: verum