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

nm1 = nm2

hence
PairFunc is one-to-one
by FUNCT_2:19; :: according to FUNCT_2:def 4 :: thesis: PairFunc is onto 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;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

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

i in rng PairFunc

then
NAT c= rng PairFunc
;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;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

then NAT = rng PairFunc ;

hence PairFunc is onto ; :: thesis: verum