let F be non degenerated comRing; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F) holds deg ((Deriv F) . p) < deg p
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: deg ((Deriv F) . p) < deg p
set q = (Deriv F) . p;
p <> 0_. F ;
then len p <> 0 by POLYNOM4:5;
then reconsider lp = (len p) - 1 as Element of NAT by INT_1:3;

now :: thesis: for i being Nat st i >= lp holds
((Deriv F) . p) . i = 0. F

let i be Nat; :: thesis: ( i >= lp implies ((Deriv F) . p) . i = 0. F )
assume i >= lp ; :: thesis: ((Deriv F) . p) . i = 0. F
then i + 1 >= ((len p) - 1) + 1 by XREAL_1:7;
then p . (i + 1) = 0. F by ALGSEQ_1:8;
hence ((Deriv F) . p) . i = (i + 1) * (0. F) by RINGDER1:def 8
.= 0. F ;
:: thesis: verum

end;

then lp is_at_least_length_of (Deriv F) . p by ALGSEQ_1:def 2;
then len ((Deriv F) . p) <= lp by ALGSEQ_1:def 3;
then (len ((Deriv F) . p)) + 1 <= ((len p) - 1) + 1 by XREAL_1:7;
then len ((Deriv F) . p) < len p by NAT_1:13;
then (len ((Deriv F) . p)) - 1 < (len p) - 1 by XREAL_1:14;
then deg ((Deriv F) . p) < (len p) - 1 by HURWITZ:def 2;
hence deg ((Deriv F) . p) < deg p by HURWITZ:def 2; :: thesis: verum