let F be 0 -characteristic Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F) holds
( (Deriv F) . p = 0_. F iff p is constant )
let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( (Deriv F) . p = 0_. F iff p is constant )

now :: thesis: ( (Deriv F) . p = 0_. F implies p is constant )

assume (Deriv F) . p = 0_. F ; :: thesis: p is constant
then A1: deg ((Deriv F) . p) = - 1 by HURWITZ:20;

per cases ( p is zero or not p is zero ) ;

suppose p is zero ; :: thesis: p is constant

hence p is constant ; :: thesis: verum

end;

suppose not p is zero ; :: thesis: p is constant

then deg ((Deriv F) . p) = (deg p) - 1 by mm6c;
hence p is constant by A1, RING_4:def 4; :: thesis: verum

end;

end;

end;

hence ( (Deriv F) . p = 0_. F iff p is constant ) by der4; :: thesis: verum