proposition: Lemma continuous_composition_at_2arg: forall (W X Y Z:TopologicalSpace) (f:X -> Y -> Z) (g:W -> X) (h:W -> Y) (w:W), continuous_at_2arg f (g w) (h w) -> continuous_at g w -> continuous_at h w -> continuous_at (fun w:W => f (g w) (h w)) w.
proof: Proof. intros. red in H. apply (continuous_composition_at (fun p:ProductTopology2 X Y => f (fst p) (snd p)) (fun w:W => (g w, h w))); trivial. now apply product2_map_continuous_at. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)