[STATEMENT]
lemma continuous_on_components:
 fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
  assumes "locally connected S " "\<And>C. C \<in> components S \<Longrightarrow> continuous_on C f"
  shows "continuous_on S f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S f
[PROOF STEP]
proof (rule continuous_on_components_gen)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. C \<in> components S \<Longrightarrow> openin (top_of_set S) C \<and> continuous_on C f
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. C \<in> components S \<Longrightarrow> openin (top_of_set S) C \<and> continuous_on C f
[PROOF STEP]
assume "C \<in> components S"
[PROOF STATE]
proof (state)
this:
C \<in> components S

goal (1 subgoal):
 1. \<And>C. C \<in> components S \<Longrightarrow> openin (top_of_set S) C \<and> continuous_on C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> components S
[PROOF STEP]
show "openin (top_of_set S) C \<and> continuous_on C f"
[PROOF STATE]
proof (prove)
using this:
C \<in> components S

goal (1 subgoal):
 1. openin (top_of_set S) C \<and> continuous_on C f
[PROOF STEP]
by (simp add: assms openin_components_locally_connected)
[PROOF STATE]
proof (state)
this:
openin (top_of_set S) C \<and> continuous_on C f

goal:
No subgoals!
[PROOF STEP]
qed