src/HOL/Analysis/Path_Connected.thy

   obtain y where x: "x = p y" and y: "0 \<le> y" "y \<le> 1"
     using x by (auto simp: path_image_def)
   show ?thesis
     unfolding path_component_def 
   proof (intro exI conjI)
-    have "continuous_on {0..1} (p \<circ> (( *) y))"
+    have "continuous_on {0..1} (p \<circ> ((*) y))"
       apply (rule continuous_intros)+
       using p [unfolded path_def] y
       apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
       done
     then show "path (\<lambda>u. p (y * u))"