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,1) holds
(Der1 R) . f = anpoly (a,0)
let f be Element of the carrier of (Polynom-Ring R); :: thesis: for a being Element of R st f = anpoly (a,1) holds
(Der1 R) . f = anpoly (a,0)
let a be Element of R; :: thesis: ( f = anpoly (a,1) implies (Der1 R) . f = anpoly (a,0) )
reconsider f1 = f as Polynomial of R ;
assume A1: f = anpoly (a,1) ; :: thesis: (Der1 R) . f = anpoly (a,0)
for n being Element of NAT holds ((Der1 R) . f) . n = (anpoly (a,0)) . n

proof

let n be Element of NAT ; :: thesis: ((Der1 R) . f) . n = (anpoly (a,0)) . n

per cases ( n = 0 or n <> 0 ) ;

suppose A2: n = 0 ; :: thesis: ((Der1 R) . f) . n = (anpoly (a,0)) . n

then ((Der1 R) . f) . n = (0 + 1) * (f1 . (0 + 1)) by Def8
.= 1 * a by A1, POLYDIFF:24
.= a by BINOM:13
.= (anpoly (a,0)) . n by A2, POLYDIFF:24 ;
hence ((Der1 R) . f) . n = (anpoly (a,0)) . n ; :: thesis: verum

end;

suppose A3: n <> 0 ; :: thesis: ((Der1 R) . f) . n = (anpoly (a,0)) . n

then A4: n + 1 <> 1 ;
((Der1 R) . f) . n = (n + 1) * ((anpoly (a,1)) . (n + 1)) by A1, Def8
.= (n + 1) * (0. R) by A4, POLYDIFF:25
.= 0. R by Th3
.= (anpoly (a,0)) . n by A3, POLYDIFF:25 ;
hence ((Der1 R) . f) . n = (anpoly (a,0)) . n ; :: thesis: verum

end;

end;

end;

hence (Der1 R) . f = anpoly (a,0) ; :: thesis: verum