theorem Th25: :: E_TRANS2:22

for j being Nat
for u being Element of the carrier of (Polynom-Ring INT.Ring) holds eval ((~ ((tau j) * u)),(In (j,INT.Ring))) = 0. INT.Ring