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
((Der1 INT.Ring) |^ k) . (f |^ k) = (k !) * (1. (Polynom-Ring INT.Ring))
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 ((Der1 INT.Ring) |^ k) . (f |^ k) = (k !) * (1. (Polynom-Ring INT.Ring)) )
assume A1: ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) ; :: thesis: ((Der1 INT.Ring) |^ k) . (f |^ k) = (k !) * (1. (Polynom-Ring INT.Ring))
A2: f |^ 0 = 1_ (Polynom-Ring INT.Ring) by BINOM:8
.= 1. (Polynom-Ring INT.Ring) ;
A3: eta (k,k) = (k !) / (0 !) by XREAL_1:232
.= k ! by NEWTON:12 ;

per cases ( k <> 0 or k = 0 ) ;

suppose k <> 0 ; :: thesis: ((Der1 INT.Ring) |^ k) . (f |^ k) = (k !) * (1. (Polynom-Ring INT.Ring))

then ( 1 <= k & k <= k ) by NAT_1:14;
then ((Der1 INT.Ring) |^ k) . (f |^ k) = (k !) * (f |^ (k -' k)) by A3, Th19, A1
.= (k !) * (1. (Polynom-Ring INT.Ring)) by A2, XREAL_1:232 ;
hence ((Der1 INT.Ring) |^ k) . (f |^ k) = (k !) * (1. (Polynom-Ring INT.Ring)) ; :: thesis: verum

end;

suppose A5: k = 0 ; :: thesis: ((Der1 INT.Ring) |^ k) . (f |^ k) = (k !) * (1. (Polynom-Ring INT.Ring))

(Der1 INT.Ring) |^ 0 = id (Polynom-Ring INT.Ring) by VECTSP11:18;
hence ((Der1 INT.Ring) |^ k) . (f |^ k) = (k !) * (1. (Polynom-Ring INT.Ring)) by A2, A5, NEWTON:12, BINOM:13; :: thesis: verum

end;

end;