src/HOL/Analysis/Abstract_Topology_2.thy

       and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
     shows "continuous_map X Y g"
   unfolding continuous_map_openin_preimage_eq
 proof (intro conjI allI impI)
   show "g ` topspace X \<subseteq> topspace Y"
-    using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce
+    using g cont continuous_map_image_subset_topspace by fastforce
 next
   fix U
   assume Y: "openin Y U"
   have T: "T i \<subseteq> topspace X" if "i \<in> I" for i
     using ope by (simp add: openin_subset that)

     and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
   shows "continuous_map X Y g"
   unfolding continuous_map_closedin_preimage_eq
 proof (intro conjI allI impI)
   show "g ` topspace X \<subseteq> topspace Y"
-    using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce
+    using g cont continuous_map_image_subset_topspace by fastforce
 next
   fix U
   assume Y: "closedin Y U"
   have T: "T i \<subseteq> topspace X" if "i \<in> I" for i
     using clo by (simp add: closedin_subset that)