let R be domRing; :: thesis: for f being Element of the carrier of (Polynom-Ring R) st len f > 1 & Char R = 0 holds
len ((Der1 R) . f) = (len f) - 1
let f be Element of the carrier of (Polynom-Ring R); :: thesis: ( len f > 1 & Char R = 0 implies len ((Der1 R) . f) = (len f) - 1 )
reconsider n = 0 as Nat ;
assume A1: ( len f > 1 & Char R = 0 ) ; :: thesis: len ((Der1 R) . f) = (len f) - 1
then A2: (len f) - 1 > 1 - 1 by XREAL_1:14;
reconsider lf1 = (len f) - 1 as Nat by A1;
lf1 + 0 > 0 by A2;
then A4: lf1 >= 1 by NAT_1:19;
reconsider lf2 = lf1 - 1 as Nat by A2;
A5: lf1 + 1 = len f ;
for i being Nat st i >= lf1 holds
((Der1 R) . f) . i = 0. R

proof

let i be Nat; :: thesis: ( i >= lf1 implies ((Der1 R) . f) . i = 0. R )
assume i >= lf1 ; :: thesis: ((Der1 R) . f) . i = 0. R
then i + 1 >= lf1 + 1 by XREAL_1:6;
then A8: f . (i + 1) = 0. R by ALGSEQ_1:8;
((Der1 R) . f) . i = (i + 1) * (f . (i + 1)) by RINGDER1:def 8
.= 0. R by A8 ;
hence ((Der1 R) . f) . i = 0. R ; :: thesis: verum

end;

then A9: lf1 is_at_least_length_of (Der1 R) . f ;
A10: ((Der1 R) . f) . lf2 = (lf2 + 1) * (f . (lf2 + 1)) by RINGDER1:def 8
.= lf1 * (f . lf1) ;
reconsider flf1 = f . lf1 as Element of R ;
not flf1 is zero by A5, ALGSEQ_1:10;
hence len ((Der1 R) . f) = (len f) - 1 by Th15, A4, A9, A10, A1, Th12; :: thesis: verum