let R be non degenerated comRing; :: thesis: for m being Nat
for x being Element of R
for D being Derivation of R holds D . (x |^ (m + 1)) = (m + 1) * ((x |^ m) * (D . x))
let m be Nat; :: thesis: for x being Element of R
for D being Derivation of R holds D . (x |^ (m + 1)) = (m + 1) * ((x |^ m) * (D . x))
let x be Element of R; :: thesis: for D being Derivation of R holds D . (x |^ (m + 1)) = (m + 1) * ((x |^ m) * (D . x))
let D be Derivation of R; :: thesis: D . (x |^ (m + 1)) = (m + 1) * ((x |^ m) * (D . x))
defpred S₁[ Nat] means D . (x |^ ($1 + 1)) = ($1 + 1) * ((x |^ $1) * (D . x));
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
set t = n + 1;
A3: x |^ ((n + 1) + 1) = (x |^ 1) * (x |^ (n + 1)) by BINOM:10
.= x * (x |^ (n + 1)) by BINOM:8 ;
D . (x |^ ((n + 1) + 1)) = (x * ((n + 1) * ((x |^ n) * (D . x)))) + ((x |^ (n + 1)) * (D . x)) by A2, Def1, A3
.= ((n + 1) * (x * ((x |^ n) * (D . x)))) + ((x |^ (n + 1)) * (D . x)) by BINOM:19
.= ((n + 1) * ((x * (x |^ n)) * (D . x))) + ((x |^ (n + 1)) * (D . x)) by GROUP_1:def 3
.= ((n + 1) * (((x |^ 1) * (x |^ n)) * (D . x))) + ((x |^ (n + 1)) * (D . x)) by BINOM:8
.= ((n + 1) * ((x |^ (n + 1)) * (D . x))) + ((x |^ (n + 1)) * (D . x)) by BINOM:10
.= ((n + 1) * ((x |^ (n + 1)) * (D . x))) + (1 * ((x |^ (n + 1)) * (D . x))) by BINOM:13
.= ((n + 1) + 1) * ((x |^ (n + 1)) * (D . x)) by BINOM:15 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(0 + 1) * ((x |^ 0) * (D . x)) = 1 * ((1_ R) * (D . x)) by BINOM:8
.= D . x by BINOM:13
.= D . (x |^ (0 + 1)) by BINOM:8 ;
then A4: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence D . (x |^ (m + 1)) = (m + 1) * ((x |^ m) * (D . x)) ; :: thesis: verum