proposition: Lemma Rmult_continuous: continuous_2arg Rmult (X:=RTop) (Y:=RTop) (Z:=RTop).
proof: Proof. apply pointwise_continuity_2arg. intros x0 y0. red. match goal with |- continuous_at ?f ?q => replace f with (fun p:point_set RTop*point_set RTop => (fst p - x0) * (snd p - y0) + y0 * fst p + x0 * snd p - x0 * y0) end. 2: { extensionality p. destruct p. simpl. ring. } apply diff_continuous. 2: { apply continuous_func_continuous_everywhere; apply continuous_constant. } apply sum_continuous. 2: { apply const_multiple_continuous, continuous_func_continuous_everywhere; apply product2_snd_continuous. } apply sum_continuous. 2: { apply const_multiple_continuous, continuous_func_continuous_everywhere; apply product2_fst_continuous. } apply continuous_composition_at_2arg with RTop RTop. - simpl. replace (x0-x0) with 0 by ring. replace (y0-y0) with 0 by ring. apply Rmult_continuous_at_origin. - apply diff_continuous; apply continuous_func_continuous_everywhere; apply product2_fst_continuous + apply continuous_constant. - apply diff_continuous; apply continuous_func_continuous_everywhere; apply product2_snd_continuous + apply continuous_constant. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)