theorem Th18: :: E_TRANS1:18

for L being domRing
for D being Derivation of L
for f being Element of the carrier of L
for j, n being Nat holds (D |^ n) . (j * f) = j * ((D |^ n) . f)