let R be non degenerated comRing; :: thesis: for p being Element of the carrier of (Polynom-Ring R) holds (Deriv R) . (p |^ 0) = 0_. R
let p be Element of the carrier of (Polynom-Ring R); :: thesis: (Deriv R) . (p |^ 0) = 0_. R
p |^ 0 = 1_ (Polynom-Ring R) by BINOM:8
.= 1_. R by POLYNOM3:def 10 ;
hence (Deriv R) . (p |^ 0) = 0_. R by der1; :: thesis: verum