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

now :: thesis: for n, m being Element of NAT holds N1 . (n,m) = N2 . (n,m)

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

end;

hence N1 = N2 ; :: thesis: verum