We will prove power_real ω = R_omega_space.
Use reflexivity.
∎