proposition: Corollary sin_continuous : @continuous RTop RTop sin.
proof: Proof. apply continuous_iff_continuity. apply continuity_sin. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)