We will prove complete_metric_space R_omega_space Romega_D_metric.

rewrite the current goal using (power_real_omega_eq_Romega_space) (from right to left).

rewrite the current goal using (bounded_product_metric_eq_Romega_D_metric) (from right to left).

An exact proof term for the current goal is product_Romega_complete.

∎