theorem Th27: :: E_TRANS2:24

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