let N1, N2 be Function of [:NAT,NAT:],NAT; :: thesis: ( ( for n, m being Element of NAT holds N1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) & ( for n, m being Element of NAT holds N2 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) implies N1 = N2 )
assume that
A3: for n, m being Element of NAT holds N1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 and
A4: for n, m being Element of NAT holds N2 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ; :: thesis: N1 = N2

now

let n, m be Element of NAT ; :: thesis: N1 . (n,m) = N2 . (n,m)
N1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 by A3;
hence N1 . (n,m) = N2 . (n,m) by A4; :: thesis: verum

end;

hence N1 = N2 by BINOP_1:2; :: thesis: verum