let R be non degenerated comRing; :: thesis: for D being Derivation of R
for n being Nat
for x being Element of R holds (D |^ (n + 1)) . x = D . ((D |^ n) . x)
let D be Derivation of R; :: thesis: for n being Nat
for x being Element of R holds (D |^ (n + 1)) . x = D . ((D |^ n) . x)
let n be Nat; :: thesis: for x being Element of R holds (D |^ (n + 1)) . x = D . ((D |^ n) . x)
let x be Element of R; :: thesis: (D |^ (n + 1)) . x = D . ((D |^ n) . x)
A1: dom (D |^ n) = the carrier of R by Th8;
(D |^ (n + 1)) . x = (D * (D |^ n)) . x by Th8
.= D . ((D |^ n) . x) by A1, FUNCT_1:13 ;
hence (D |^ (n + 1)) . x = D . ((D |^ n) . x) ; :: thesis: verum