let F be 0 -characteristic Field; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F) holds deg ((Deriv F) . p) = (deg p) - 1
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: deg ((Deriv F) . p) = (deg p) - 1
H: Char F = 0 by RING_3:def 6;

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

suppose p is constant ; :: thesis: deg ((Deriv F) . p) = (deg p) - 1

then ( deg p = 0 & (Deriv F) . p = 0_. F ) by der4, RING_4:def 4;
hence deg ((Deriv F) . p) = (deg p) - 1 by HURWITZ:20; :: thesis: verum

end;

suppose not p is constant ; :: thesis: deg ((Deriv F) . p) = (deg p) - 1

then A: deg p > 0 by RING_4:def 4;
then reconsider n = (deg p) - 1 as Element of NAT by INT_1:3;
set q = (Deriv F) . p;
B: p . (deg p) = LC p by FIELD_6:2;
((Deriv F) . p) . n = (n + 1) * (p . (n + 1)) by RINGDER1:def 8
.= (deg p) '*' (p . (deg p)) by RING_3:def 2 ;
then ((Deriv F) . p) . n <> 0. F by H, A, B, REALALG2:25;
then D: len ((Deriv F) . p) >= n + 1 by NAT_1:13, ALGSEQ_1:8;
deg ((Deriv F) . p) < deg p by mm6a;
then (len ((Deriv F) . p)) - 1 < deg p by HURWITZ:def 2;
then ((len ((Deriv F) . p)) - 1) + 1 < (deg p) + 1 by XREAL_1:6;
then len ((Deriv F) . p) <= n + 1 by NAT_1:13;
then len ((Deriv F) . p) = n + 1 by D, XXREAL_0:1;
hence deg ((Deriv F) . p) = (deg p) - 1 by HURWITZ:def 2; :: thesis: verum

end;

end;