theorem Th10: :: NAT_2:10

for k, n being Nat st k <= n holds
2 to_power n = (2 to_power k) * (2 to_power (n -' k))