thus PairFunc is one-to-one :: according to FUNCT_2:def 4 :: thesis: PairFunc is onto

proof

now

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

end;

hence PairFunc is one-to-one by FUNCT_2:25; :: thesis: verum

end;

thus PairFunc is onto :: thesis: verum

proof

now

let i be set ; :: thesis: ( i in NAT implies i in rng PairFunc )
assume i in NAT ; :: thesis: i in rng PairFunc
then reconsider i' = i as Element of NAT ;
consider n, m being Element of NAT such that
A4: i' + 1 = (2 |^ n) * ((2 * m) + 1) by Th1;
( i' - 0 = ((2 |^ n) * ((2 * m) + 1)) - 1 & dom PairFunc = [:NAT ,NAT :] ) by A4, FUNCT_2:def 1;
then ( [n,m] in dom PairFunc & i = PairFunc . [n,m] ) by Def1;
hence i in rng PairFunc by FUNCT_1:def 5; :: thesis: verum

end;

then ( NAT c= rng PairFunc & rng PairFunc c= NAT ) by TARSKI:def 3;
hence NAT = rng PairFunc by XBOOLE_0:def 10; :: according to FUNCT_2:def 3 :: thesis: verum

end;