set L = Polynom-Ring INT.Ring;
set D = Der1 INT.Ring;
let k be Nat; :: thesis: for f being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) holds
for j being Nat st 1 <= j & j <= k holds
((Der1 INT.Ring) |^ j) . (f |^ k) = (eta (k,j)) * (f |^ (k -' j))
let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) implies for j being Nat st 1 <= j & j <= k holds
((Der1 INT.Ring) |^ j) . (f |^ k) = (eta (k,j)) * (f |^ (k -' j)) )
assume A1: ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) ; :: thesis: for j being Nat st 1 <= j & j <= k holds
((Der1 INT.Ring) |^ j) . (f |^ k) = (eta (k,j)) * (f |^ (k -' j))
A2: (Der1 INT.Ring) . f = ((Der1 INT.Ring) |^ 1) . f by VECTSP11:19
.= 1. (Polynom-Ring INT.Ring) by A1, BINOM:8 ;
defpred S₁[ Nat] means for j being Nat st 1 <= j & j <= $1 holds
((Der1 INT.Ring) |^ j) . (f |^ $1) = (eta ($1,j)) * (f |^ ($1 -' j));
A3: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A4: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
for l being Nat st 1 <= l & l <= k holds
((Der1 INT.Ring) |^ l) . (f |^ k) = (eta (k,l)) * (f |^ (k -' l))

proof

let l be Nat; :: thesis: ( 1 <= l & l <= k implies ((Der1 INT.Ring) |^ l) . (f |^ k) = (eta (k,l)) * (f |^ (k -' l)) )
assume A5: ( 1 <= l & l <= k ) ; :: thesis: ((Der1 INT.Ring) |^ l) . (f |^ k) = (eta (k,l)) * (f |^ (k -' l))
then reconsider k1 = k - 1 as Nat ;
A6: k -' 1 = k1 by A5, XXREAL_0:2, XREAL_1:233;
A7: ((Der1 INT.Ring) |^ 1) . (f |^ k) = (Der1 INT.Ring) . (f |^ (k1 + 1)) by VECTSP11:19
.= (k1 + 1) * ((f |^ k1) * (1. (Polynom-Ring INT.Ring))) by A2, RINGDER1:7
.= k * (f |^ (k -' 1)) ;
A8: eta (k,1) = ((k1 + 1) * (k1 !)) / (k1 !) by NEWTON:15
.= k by XCMPLX_1:89 ;
reconsider l1 = l - 1 as Nat by A5;
A9: ((Der1 INT.Ring) |^ l) . (f |^ k) = ((Der1 INT.Ring) |^ (l1 + 1)) . (f |^ k)
.= (((Der1 INT.Ring) |^ l1) * ((Der1 INT.Ring) |^ 1)) . (f |^ k) by VECTSP11:20
.= ((Der1 INT.Ring) |^ l1) . (k * (f |^ k1)) by A7, A6, FUNCT_2:15
.= k * (((Der1 INT.Ring) |^ l1) . (f |^ k1)) by Th18 ;
A10: k1 < k - 0 by XREAL_1:15;
A11: k1 -' l1 = (k - 1) - (l - 1) by A5, XREAL_1:9, XREAL_1:233
.= k - l
.= k -' l by A5, XREAL_1:233 ;
then A12: k * (eta (k1,l1)) = ((k1 + 1) * (k1 !)) / ((k -' l) !)
.= eta (k,l) by NEWTON:15 ;
reconsider s = eta (k1,l1), k = k as Element of NAT by ORDINAL1:def 12;
reconsider t = f |^ (k1 -' l1) as Element of (Polynom-Ring INT.Ring) ;

per cases ( 1 <= l1 or 1 > l1 ) ;

suppose 1 <= l1 ; :: thesis: ((Der1 INT.Ring) |^ l) . (f |^ k) = (eta (k,l)) * (f |^ (k -' l))

then ( 1 <= l1 & l1 <= k1 ) by A5, XREAL_1:9;
then k * (((Der1 INT.Ring) |^ l1) . (f |^ k1)) = k * (s * t) by A10, A4
.= (eta (k,l)) * (f |^ (k -' l)) by A11, A12, Lm11 ;
hence ((Der1 INT.Ring) |^ l) . (f |^ k) = (eta (k,l)) * (f |^ (k -' l)) by A9; :: thesis: verum

end;

suppose 1 > l1 ; :: thesis: ((Der1 INT.Ring) |^ l) . (f |^ k) = (eta (k,l)) * (f |^ (k -' l))

then l1 = 0 by NAT_1:14;
hence ((Der1 INT.Ring) |^ l) . (f |^ k) = (eta (k,l)) * (f |^ (k -' l)) by A7, A8; :: thesis: verum

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(A3);
hence for j being Nat st 1 <= j & j <= k holds
((Der1 INT.Ring) |^ j) . (f |^ k) = (eta (k,j)) * (f |^ (k -' j)) ; :: thesis: verum