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

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)

hence
N1 = N2
; :: thesis: verumlet 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;N1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 by A4;

hence N1 . (n,m) = N2 . (n,m) by A5; :: thesis: verum