proposition: Lemma product2_snd_continuous: continuous (@snd X Y) (X:=ProductTopology2).
proof: Proof. exact (weak_topology_makes_continuous_funcs _ _ _ prod2_proj twoT_2). Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)