let R be domRing; :: thesis: for f being Element of the carrier of (Polynom-Ring R)
for j being Nat st len f > j & Char R = 0 holds
len (((Der1 R) |^ j) . f) = (len f) - j
let f be Element of the carrier of (Polynom-Ring R); :: thesis: for j being Nat st len f > j & Char R = 0 holds
len (((Der1 R) |^ j) . f) = (len f) - j
let j be Nat; :: thesis: ( len f > j & Char R = 0 implies len (((Der1 R) |^ j) . f) = (len f) - j )
assume A1: ( len f > j & Char R = 0 ) ; :: thesis: len (((Der1 R) |^ j) . f) = (len f) - j
reconsider lf1 = (len f) - 1 as Nat by A1;
A2: (len f) - j > j - j by A1, XREAL_1:14;
(len f) - j in NAT by A2, INT_1:3;
then reconsider lfj = (len f) - j as Nat ;
lfj + 0 > 0 by A2;
then A4: lfj >= 1 by NAT_1:19;
reconsider lfj2 = lfj - 1 as Nat by A2;
A5: lf1 + 1 = len f ;
reconsider lfjcoef = ((lfj2 + j) choose lfj2) * (j !) as Nat ;
A6: eta ((lfj2 + j),j) = ((lfj2 + j) choose j) * (j !) by Th17, XREAL_1:38;
reconsider l = lfj2 + j as Nat ;
( lfj2 = l - j & j <= l ) by XREAL_1:38;
then (lfj2 + j) choose j = l choose lfj2 by NEWTON:20;
then A9: (((Der1 R) |^ j) . f) . lfj2 = lfjcoef * (f . lf1) by A6, Th22;
reconsider lfjcoef = ((lfj2 + j) choose lfj2) * (j !) as Nat ;
reconsider flf1 = f . lf1 as Element of R ;
for k being Element of R st k <> 0. R holds
not k is zero ;
then A11: flf1 is non zero Element of R by A5, ALGSEQ_1:10;
reconsider m1 = j ! as Nat ;
reconsider m2 = (lfj2 + j) choose lfj2 as Nat ;
A12: for i being Nat st i >= lfj holds
(((Der1 R) |^ j) . f) . i = 0. R

proof

let i be Nat; :: thesis: ( i >= lfj implies (((Der1 R) |^ j) . f) . i = 0. R )
assume i >= lfj ; :: thesis: (((Der1 R) |^ j) . f) . i = 0. R
then i + j >= ((len f) - j) + j by XREAL_1:6;
then A15: f . (i + j) = 0. R by ALGSEQ_1:8;
reconsider l = i + j as Nat ;
(((Der1 R) |^ j) . f) . i = (eta ((i + j),j)) * (f . (i + j)) by Th22
.= 0. R by A15 ;
hence (((Der1 R) |^ j) . f) . i = 0. R ; :: thesis: verum

end;

lfj is_at_least_length_of ((Der1 R) |^ j) . f by A12;
hence len (((Der1 R) |^ j) . f) = (len f) - j by Th15, A4, A9, A1, A11, Th12; :: thesis: verum