let i be Nat; :: thesis: Roots (tau i) = {(In (i,INT.Ring))}
reconsider x = i as Element of INT.Ring by INT_1:def 2;
Roots <%(In ((- i),INT.Ring)),(1. INT.Ring)%> = Roots <%(- x),(1. INT.Ring)%>
.= {(In (i,INT.Ring))} by UPROOTS:48 ;
hence Roots (tau i) = {(In (i,INT.Ring))} ; :: thesis: verum