let R be non degenerated comRing; :: thesis: for n being Nat
for D being Derivation of R holds
( D |^ (n + 1) = D * (D |^ n) & dom D = the carrier of R & dom (D |^ n) = the carrier of R & D |^ n is the carrier of R -valued Function )
let n be Nat; :: thesis: for D being Derivation of R holds
( D |^ (n + 1) = D * (D |^ n) & dom D = the carrier of R & dom (D |^ n) = the carrier of R & D |^ n is the carrier of R -valued Function )
let D be Derivation of R; :: thesis: ( D |^ (n + 1) = D * (D |^ n) & dom D = the carrier of R & dom (D |^ n) = the carrier of R & D |^ n is the carrier of R -valued Function )
D |^ 1 = D by VECTSP11:19;
hence ( D |^ (n + 1) = D * (D |^ n) & dom D = the carrier of R & dom (D |^ n) = the carrier of R & D |^ n is the carrier of R -valued Function ) by FUNCT_2:def 1, VECTSP11:20; :: thesis: verum