theorem :: NTALGO_2:13

for m being Element of NAT holds ALGO_BPOW (0,0,m) = 1