let F be non degenerated comRing; :: thesis: for p being constant Element of the carrier of (Polynom-Ring F) holds (Deriv F) . p = 0_. F
let p be constant Element of the carrier of (Polynom-Ring F); :: thesis: (Deriv F) . p = 0_. F
consider a being Element of F such that
A: p = a | F by RING_4:20;
B: ( 1. (Polynom-Ring F) = 1_. F & 0. (Polynom-Ring F) = 0_. F ) by POLYNOM3:def 10;
thus (Deriv F) . p = (Deriv F) . (a * (1_. F)) by A, RING_4:16
.= a * ((Deriv F) . (1. (Polynom-Ring F))) by B, der3
.= a * (0_. F) by B, der1
.= 0_. F by POLYNOM5:28 ; :: thesis: verum