proposition: Lemma continuous_2arg_func_continuous_everywhere: continuous_2arg -> forall (x:X) (y:Y), continuous_at_2arg x y.
proof: Proof. intros. now apply continuous_func_continuous_everywhere. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)