theorem :: AOFA_I00:12

for n, m being Nat holds 0 to_power (n + m) = (0 to_power n) * (0 to_power m)