proposition: Lemma product_space_proj_continuous: forall a:A, continuous (product_space_proj a) (X:=ProductTopology).
proof: Proof. apply weak_topology_makes_continuous_funcs. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)