proposition: Lemma const_multiple_func_continuous: forall c:R, continuous (fun x:R => c*x) (X:=RTop) (Y:=RTop).
proof: Proof. intros. apply continuous_iff_continuity, continuity_mult. - apply continuity_const. red. now intros. - intro. apply derivable_continuous_pt, derivable_pt_id. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)