let j be Nat; :: thesis: for u being Element of the carrier of (Polynom-Ring INT.Ring) holds eval ((~ ((tau j) * u)),(In (j,INT.Ring))) = 0. INT.Ring
let u be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: eval ((~ ((tau j) * u)),(In (j,INT.Ring))) = 0. INT.Ring
Roots (tau j) = {(In (j,INT.Ring))} by Lm4;
then In (j,INT.Ring) in Roots (tau j) by TARSKI:def 1;
then In (j,INT.Ring) is_a_root_of tau j by POLYNOM5:def 10;
then A1: eval ((tau j),(In (j,INT.Ring))) = 0. INT.Ring by POLYNOM5:def 7;
eval ((~ ((tau j) * u)),(In (j,INT.Ring))) = eval (((~ (tau j)) *' (~ u)),(In (j,INT.Ring))) by POLYNOM3:def 10
.= (0. INT.Ring) * (eval ((~ u),(In (j,INT.Ring)))) by A1, POLYNOM4:24
.= 0. INT.Ring ;
hence eval ((~ ((tau j) * u)),(In (j,INT.Ring))) = 0. INT.Ring ; :: thesis: verum