:: deftheorem Def3A defines TRANQN DIOPHAN2:def 4 :
for b₁ being Function of RAT,NAT holds
( b₁ = TRANQN iff for x being Rational holds b₁ . x = denominator x );