:: deftheorem defines tau E_TRANS2:def 2 :
for i being Nat holds tau i = <%(In ((- i),INT.Ring)),(1. INT.Ring)%>;