let k, n be Nat; :: thesis: ( k <= n implies 2 to_power n = (2 to_power k) * (2 to_power (n -' k)) )
assume k <= n ; :: thesis: 2 to_power n = (2 to_power k) * (2 to_power (n -' k))
then n = k + (n -' k) by XREAL_1:235;
hence 2 to_power n = (2 to_power k) * (2 to_power (n -' k)) by POWER:27; :: thesis: verum