now :: thesis: for nm1, nm2 being object st nm1 in [:NAT,NAT:] & nm2 in [:NAT,NAT:] & PairFunc . nm1 = PairFunc . nm2 holds
nm1 = nm2

let nm1, nm2 be object ; :: thesis: ( nm1 in [:NAT,NAT:] & nm2 in [:NAT,NAT:] & PairFunc . nm1 = PairFunc . nm2 implies nm1 = nm2 )
assume that
A1: nm1 in [:NAT,NAT:] and
A2: nm2 in [:NAT,NAT:] and
A3: PairFunc . nm1 = PairFunc . nm2 ; :: thesis: nm1 = nm2
consider n2, m2 being object such that
A4: ( n2 in NAT & m2 in NAT ) and
A5: [n2,m2] = nm2 by A2, ZFMISC_1:def 2;
consider n1, m1 being object such that
A6: ( n1 in NAT & m1 in NAT ) and
A7: [n1,m1] = nm1 by A1, ZFMISC_1:def 2;
reconsider n1 = n1, n2 = n2, m1 = m1, m2 = m2 as Element of NAT by A6, A4;
A8: ((2 |^ n2) * ((2 * m2) + 1)) - 1 = PairFunc . nm2 by A5, Def1;
A9: ((2 |^ n1) * ((2 * m1) + 1)) - 1 = PairFunc . nm1 by A7, Def1;
then n1 = n2 by A3, A8, CARD_4:4;
hence nm1 = nm2 by A3, A7, A5, A9, A8, CARD_4:4; :: thesis: verum

end;

hence PairFunc is one-to-one by FUNCT_2:19; :: according to FUNCT_2:def 4 :: thesis: PairFunc is onto

now :: thesis: for i being object st i in NAT holds
i in rng PairFunc

let i be object ; :: thesis: ( i in NAT implies i in rng PairFunc )
assume i in NAT ; :: thesis: i in rng PairFunc
then reconsider i9 = i as Element of NAT ;
consider n, m being Nat such that
A10: i9 + 1 = (2 |^ n) * ((2 * m) + 1) by Th1;
( n in NAT & m in NAT ) by ORDINAL1:def 12;
then A11: [n,m] in [:NAT,NAT:] by ZFMISC_1:87;
i9 - 0 = ((2 |^ n) * ((2 * m) + 1)) - 1 by A10;
then ( dom PairFunc = [:NAT,NAT:] & i = PairFunc . [n,m] ) by Def1, FUNCT_2:def 1;
hence i in rng PairFunc by FUNCT_1:def 3, A11; :: thesis: verum

end;

then NAT c= rng PairFunc ;
then NAT = rng PairFunc ;
hence PairFunc is onto ; :: thesis: verum