deffunc H1( 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:83;
then ((2 |^ n) * ((2 * m) + 1)) - 1 is Element of NAT by NAT_1:20, XREAL_1:129;
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) = H1(n,m) from BINOP_1:sch 4();
 take NN ; :: thesis: for n, m being Nat holds NN . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
let n, m be Nat; :: thesis: NN . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
A3: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
NN . (n,m) = In ((((2 |^ n) * ((2 * m) + 1)) - 1),NAT) by A2, A3
.= ((2 |^ n) * ((2 * m) + 1)) - 1 by A1, SUBSET_1:def 8, A3 ;
hence NN . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ; :: thesis: verum