:: deftheorem Def1 defines PairFunc NAGATA_2:def 1 :
for b₁ being Function of [:NAT,NAT:],NAT holds
( b₁ = PairFunc iff for n, m being Nat holds b₁ . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 );