deffunc H₁( Element of NAT , Element of NAT ) -> Element of NAT = In (((2 |^ $1) * ((2 * $2) + 1)) - 1),NAT ;
A1: for n, m being Element of NAT holds ((2 |^ n) * ((2 * m) + 1)) - 1 in NAT

proof

let n, m be Element of NAT ; :: thesis: ((2 |^ n) * ((2 * m) + 1)) - 1 in NAT
0 < 2 |^ n by NEWTON:102;
then ((2 |^ n) * ((2 * m) + 1)) - 1 is Element of NAT by NAT_1:20, XREAL_1:131;
hence ((2 |^ n) * ((2 * m) + 1)) - 1 in NAT ; :: thesis: verum

end;

consider NN being Function of [:NAT ,NAT :],NAT such that
A2: for n, m being Element of NAT holds NN . n,m = H₁(n,m) from BINOP_1:sch 4();
take NN ; :: thesis: for n, m being Element of NAT holds NN . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
let n, m be Element of NAT ; :: thesis: NN . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
NN . n,m = In (((2 |^ n) * ((2 * m) + 1)) - 1),NAT by A2
.= ((2 |^ n) * ((2 * m) + 1)) - 1 by A1, FUNCT_7:def 1 ;
hence NN . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ; :: thesis: verum