let R be domRing; :: thesis: for f being Element of the carrier of (Polynom-Ring R)
for k, i being Nat holds (((Der1 R) |^ k) . f) . i = (eta ((i + k),k)) * (f . (i + k))
let f be Element of the carrier of (Polynom-Ring R); :: thesis: for k, i being Nat holds (((Der1 R) |^ k) . f) . i = (eta ((i + k),k)) * (f . (i + k))
let k be Nat; :: thesis: for i being Nat holds (((Der1 R) |^ k) . f) . i = (eta ((i + k),k)) * (f . (i + k))
set D = Der1 R;
set PR = Polynom-Ring R;
defpred S₁[ Nat] means for i, i being Nat holds (((Der1 R) |^ $1) . f) . i = (eta ((i + $1),$1)) * (f . (i + $1));
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
set fk = ((Der1 R) |^ k) . f;
A3: (Der1 R) . (((Der1 R) |^ k) . f) = ((Der1 R) |^ (k + 1)) . f by RINGDER1:9;
for i being Nat holds ((Der1 R) . (((Der1 R) |^ k) . f)) . i = (eta ((i + (k + 1)),(k + 1))) * (f . (i + (k + 1)))

proof

let i be Nat; :: thesis: ((Der1 R) . (((Der1 R) |^ k) . f)) . i = (eta ((i + (k + 1)),(k + 1))) * (f . (i + (k + 1)))
reconsider m1 = i + 1, m2 = eta (((i + 1) + k),k) as Element of NAT ;
reconsider fk1 = f . ((i + 1) + k) as Element of R ;
((Der1 R) . (((Der1 R) |^ k) . f)) . i = (i + 1) * ((((Der1 R) |^ k) . f) . (i + 1)) by RINGDER1:def 8
.= m1 * (m2 * fk1) by A2
.= ((i + 1) * (eta (((i + 1) + k),k))) * fk1 by Lm11
.= (eta ((i + (1 + k)),(k + 1))) * fk1 by Lm13 ;
hence ((Der1 R) . (((Der1 R) |^ k) . f)) . i = (eta ((i + (k + 1)),(k + 1))) * (f . (i + (k + 1))) ; :: thesis: verum

end;

hence S₁[k + 1] by A3; :: thesis: verum

end;

for i being Nat holds (((Der1 R) |^ 0) . f) . i = (eta ((i + 0),0)) * (f . (i + 0))

proof

let i be Nat; :: thesis: (((Der1 R) |^ 0) . f) . i = (eta ((i + 0),0)) * (f . (i + 0))
A5: eta ((i + 0),0) = 1 by XCMPLX_1:60;
(((Der1 R) |^ 0) . f) . i = ((id (Polynom-Ring R)) . f) . i by VECTSP11:18
.= (eta ((i + 0),0)) * (f . i) by A5, BINOM:13 ;
hence (((Der1 R) |^ 0) . f) . i = (eta ((i + 0),0)) * (f . (i + 0)) ; :: thesis: verum

end;

then A6: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A1);
hence for i being Nat holds (((Der1 R) |^ k) . f) . i = (eta ((i + k),k)) * (f . (i + k)) ; :: thesis: verum