An exact proof term for the current goal is (product_topology_is_topology R R_standard_topology R R_standard_topology R_standard_topology_is_topology R_standard_topology_is_topology).