Let J be given.

Assume HJ: ¬ countable J.

We will prove ¬ normal_space (product_space J (const_space_family J R R_standard_topology)) (product_topology_full J (const_space_family J R R_standard_topology)).

An exact proof term for the current goal is (uncountable_product_R_not_normal J HJ).

∎