:: deftheorem Def1 defines derivation RINGDER1:def 1 :
for R being non degenerated comRing
for IT being Function of R,R holds
( IT is derivation iff for x, y being Element of R holds
( IT . (x + y) = (IT . x) + (IT . y) & IT . (x * y) = (x * (IT . y)) + (y * (IT . x)) ) );