theorem Th13: :: E_TRANS2:13

for i being Nat holds (Der1 INT.Ring) . (tau i) = 1. (Polynom-Ring INT.Ring)